MONDAY, MAY 11
Theme: Assuring AI |
| 0900 - 1000 |
Keynote: The Cognitive Shift: From Centralized Orchestration to Controllable Self-Organizing AI Collectives
Susmit Jha (DARPA) |
| 1000 - 1030 |
BREAK |
| 1030 - 1100 |
Can Your LLM Keep a Secret?
Sanjam Garg (UC Berkeley) |
| 1100 - 1130 |
Practical Formal Verification of Industrial Neural Networks in Aerospace
Cong Liu and Darren Cofer (Collins Aerospace) |
| 1130 - 1200 |
Deterministic Simulation Testing as a Strategy for High Confidence Systems
Michael Vaughn (Antithesis) |
| 1200 - 1330 |
LUNCH (on your own) |
| 1330 - 1400 |
Intrinsic AI Assurance: Metacognition and Formally Verified Reasoning in Foundation Model Agents
Sumit Jha (University of Florida) |
| 1400 - 1430 |
Toward a Formally Correct Simulator, Assembler, and Verifier for the Trainium AI Accelerator in Lean
Sean McLaughlin (Amazon Web Services) |
| 1430 - 1500 |
Government Keynote: Provable Security: Operationalizing Formal Methods for National Defense
Forrest Shull (OUSW (R&E)) |
| 1500 - 1530 |
POSTER AND DEMO SESSION | BREAK |
| 1530 - 1600 |
Autonomous Formal Methods
Joe Kiniry (Sigil Logic) |
| 1600 - 1630 |
Nitro Isolation Engine: Formally Verifying a Production Cloud Hypervisor
Nathan Chong and Rob Dockins (Amazon) |
| 1630 - 1700 |
OGhidra: Local AI For Reverse Engineering at Scale
Eddy Westbrook (Lawrence Livermore National Laboratory) |
| 1700 - 1730 |
Formally Verified Post-Quantum Cryptography at Scale
Dusan Kostic and Rod Chapman (Amazon) |
| 1730 onwards |
Galois-hosted Game Night
A relaxed evening of games, good company, and friendly-ish competition. Appetizers and refreshments will be available from 5:30–7:30 PM. |
| |
Adjourn for the day
|
| |
|
TUESDAY, MAY 12
Theme: AI as an Enabler |
| 0900 - 1000 |
Keynote: From Gold Medals to Guaranteed Reasoning: Building Mathematical Superintelligence
Tudor Achim (Harmonic) |
| 1000 - 1030 |
BREAK |
| 1030 - 1100 |
CSLib: Building a Platform for AI-assisted Formal Verification in Lean
Clark Barrett (Stanford University) |
| 1100 - 1130 |
Toward World Models for Network Defense
Andres Molina-Markham (MITRE) |
| 1130 - 1200 |
Transitioning Assurance Case Technology to Production‚ An Experience Report
Mauricio Castillo-Effen and Stephen Traub (Lockheed Martin) |
| 1200 - 1330 |
LUNCH (on your own) |
| 1330 - 1400 |
Neurosymbolic C++ Verification using Rocq
Gregory Malecha (Skylabs AI) |
| 1400 - 1430 |
AI-Enabled High-Confidence Firmware Bill of Materials Extraction
Christopher Wright (GrammaTech) |
| 1430 - 1500 |
Malware Detection using Features from Static Disassembly
Akshay Sood (GrammaTech) |
| 1500 - 1530 |
BREAK | Sponsor Showcase Poster Session |
| 1530 - 1600 |
AI as an Enabler for Business Logic Systems
Daniel Balasubramanian and Sandeep Neema (Vanderbilt University) |
| 1600 - 1630 |
Model-based Development for seL4 Microkit/Rust with Integrated Formal Methods using HAMR
John Hatcliff (Kansas State University) |
| 1630 - 1700 |
Lifecycle Attestation for a High Assurance, LLM-assisted Development Workflow
Adam Petz (University of Kansas, I2S) |
| 1700- 1730 |
Toward Neuro-Symbolic Natural Language Requirements to Verified Implementations for Model-Based Systems Engineering in SysML v2
Amer Tahat (Collins Aerospace) |
| |
Adjourn for the day
|
| 1830 |
HCSS Conference Dinner
Chart House Prime | 300 Second St., Annapolis, MD 21403
(with generous support from Amazon Web Services)
|
| |
|
WEDNESDAY, MAY 13
Theme: Beyond AI |
| 0900 - 1000 |
Keynote: Verus: Building a Practical Ecosystem of Provably Correct and Secure Code
Bryan Parno (CMU) |
| 1000 - 1030 |
BREAK |
| 1030 - 1100 |
Scaling CPS Understanding
Harald Ruess and Manfred Broy (SRI International) |
| 1100 - 1130 |
Certified Synthesis of High-Assurance Protocols and Monitors
Arthur Amorim (University of Central Florida) |
| 1130 - 1200 |
Securing Edge AI in Contested Environments: Formal Methods for Protection and Continuous Authorization
Boyd Multerer (Kry10 Corp) |
| 1200 - 1330 |
LUNCH (on your own |
| 1330 - 1400 |
HCSS Retrospective
Brad Martin (Galois) |
| 1400 - 1430 |
Translating Specifications to Safe and Efficient Code
Natarajan Shankar (SRI International) |
| 1430 - 1500 |
Towards A Formalism For Understanding Properties of Hidden Communication Systems and Weird Networks
Steve Lu (Stealth Software Technologies) |
| 1500 - 1530 |
POSTER AND DEMO SESSION I BREAK |
| 1530 - 1600 |
Maude-HCS: Formally Verifying Undetectability in Hidden Communication Systems using Statistical Model Checking
Joud Khoury (RTX BBN Technologies) |
| 1600 - 1630 |
Formal Verification of QUICstep using the Tamarin Symbolic Prover
Cyrill Krähenbühl (Princeton University) |
| |
Conference Adjourned |
