HCSS 2026 Program Agenda
| MONDAY, MAY 11 Theme: Assuring AI |
|
| 0900 - 1000 | Keynote Presentation: 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 | HCSS Retrospective Brad Martin (Galois) |
| 1400 - 1430 | Verifiable AI Artifacts via Geometry, Entropy, and Formal Methods: Specification, Auditing, Attribution, Steering, and Unlearning Sumit Jha (University of Florida) |
| 1430 - 1500 | Toward a formally correct simulator, assembler, and verifier for the Trainium AI accelerator in Lean Sean McLaughlin (Amazon Web Services) |
| 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 Enoch Wang (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 Presentation: 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 Lennart Beringer (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 |
| WEDNESDAY, MAY 13 Theme: TBD |
|
| 0900 - 1000 | Keynote Presentation: Verus: Building a Practical Ecosystem of Provably Correct and Secure Code Bryan Parno (CMU) |
| 100 - 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 | Government Keynote: TBA |
| 1400 - 1430 | Translating Specifications to Safe and Efficient Code Natarajan Shankar (SRI International) |
| 1430 - 1500 | POSTER AND DEMO SESSION I BREAK |
| 1500 - 1530 | Proactive Network Verification with 5STARS Cole Schlesinger and David Darais (Galois) |
| 1530 - 1600 | Towards A Formalism For Understanding Properties of Hidden Communication Systems and Weird Networks Steve Lu (Stealth Software Technologies) |
| 1600 - 1630 | Maude-HCS: Formally Verifying Undetectability in Hidden Communication Systems Using Statistical Model Checking Joud Khoury (RTX BBN Technologies) |
| 1630 - 1700 | Formal Verification of QUICstep Using the Tamarin Symbolic Prover Cryill Krahenbuehl (Princeton University) |
| Conference Adjourned | |
