HCSS 2025 Program Agenda
The HCSS Conference will be held May 12-14, 2025.
The co-located Software Certification Consortium (SCC) Meeting and the Trusted Computing Center of Excellence (TCCoE) Summit will be held May 15-16.
| MONDAY, MAY 12 Theme: Formal Verification of AI/ML Systems |
|
| 0900 - 1000 | Keynote Presentation: From Neural Network Verification to Formally Verifying Neuro-Symbolic Artificial Intelligence (AI) Taylor Johnson, Vanderbilt University |
| 1000 - 1030 | BREAK |
| 1030 - 1100 | AI for Formal Verification and Formal Verification for AI David Dalrymple, ARIA |
| 1100 - 1130 | VeriX: Verified Explainability of Deep Neural Networks Min Wu, Stanford |
| 1130 - 1200 | Semantic Verification of Foundation Models Using Mechanistic Verification and Concept Probes Susmit Jha, SRI |
| 1200 - 1330 | LUNCH (on your own) |
| Theme: Formalizing Pure Math | |
| 1330 - 1430 | Keynote Presentation: Verified Collaboration: How Lean is Transforming Mathematics, Programming, and AI Leonardo De Moura, Lean FRO and AWS |
| 1430 - 1500 | Reasoning-Enabling Representations of Math Challenges Marijn Heule, CMU |
| 1500 - 1530 | Poster Session / Break |
| 1530 - 1600 | Future Program: Exponentiating Mathematics (expMath) Patrick Shafto, DARPA |
| 1600 - 1630 | Neuro-Symbolic Techniques for LLM-based Code Generation and Auto-Formalization of Proofs Prithwish Jana and Vijay Ganesh, Georgia Institute of Technology |
| 1630 - 1700 | From Modal Logic to Computing: The Case for Hybrid Logics in Formal Methods William Harrison, Galois |
| 1700 | Adjourn for the day |
| TUESDAY, MAY 13 Theme: Novel Automated Reasoning Applications |
|
| 0900 - 1000 | Keynote Presentation: Formal Verification of Financial Infrastructure with Imandra Grant Passmore, Imandra |
| 1000 - 1030 | BREAK |
| 1030 - 1100 | Automated Reasoning for UAV Safety & Security: The DATUM Protocol Stack Max Taylor, Idaho National Laboratory |
| 1100 - 1130 | Modeling and Formal Analysis of High-Assurance Mixed-Reality Systems Junaid Babar, Collins Aerospace |
| 1130 - 1200 | Software Understanding for National Security (SUNS) Partnership Forum Report Douglas Ghormley and Christopher Harrison (SNL) |
| 1200 - 1330 | LUNCH (on your own) |
| 1330 - 1430 | HCSS 25th Anniversary Panel |
| 1430 - 1500 | An Experiment Using Layered Attestation Perry Alexander, The University of Kansas |
| 1500 - 1530 | BREAK |
| 1530 - 1600 | Formalizing and Automating the Discovery of Weird States and Machine Primitives for High-Confidence Software Meera Sridhar, University of North Carolina Charlotte |
| 1600 - 1630 | ModelForge: Using AI to Improve Security Protocols Martin Duclos, Mississippi State University |
| 1630 - 1700 | Secure Protocols via LLMs and CPSA Lauren Brandt, MITRE |
| 1700 | Adjourn for the day |
| 1830 | HCSS Conference Dinner Chart House Prime | 300 Second St, Annapolis, MD 21403 |
| WEDNESDAY, MAY 14 Theme: AI and Models in the Software Development Lifecycle |
|
| 0900 - 1000 | Keynote Presentation: Neurosymbolic Programming and the Path to Safe AI Armando Solar-Lezama, MIT CSAIL |
| 1000 - 1030 | BREAK |
| 1030 - 1100 | Reconciling Distributed System Implementation and Design with Neuro-Symbolic Reasoning Tristan Ravitch, Amazon Web Services |
| 1100 - 1130 | Translating C to Rust: Better, cheaper, faster Per Larsen, Immunant, Inc. |
| 1130 - 1200 | Functors as Bridges between AI-Generated Code and Formal Models for High-Confidence Software Systems Sumit Jha, Florida International University, Miami |
| 1200 - 1330 | LUNCH (on your own) |
| 1330 - 1400 | Secure AI Through Verification, Transparency, and Fairness Jessica Inman, GTRI |
| 1400 - 1430 | Automated SysML v2 System Model to Memory-Safe Language Code Generation with Integrated AI Assistance David Hardin, Collins Aerospace |
| 1430 - 1500 | LLM-enabled Software Testing Fanxin Kong, University of Notre Dame |
| 1500 - 1530 | Break |
| 1530 - 1600 | Towards Trustworthy Integration of Generative AI in the MBSE Development Lifecycle Amer Tahat, Collins Aerospace |
| 1600 - 1630 | Combining AI and Models to Identify Faults in Business Logic Daniel Balasubramanian, Vanderbilt University |
| 1630 - 1700 |
TCCoE & SCC Introductions HCSS Closing Remarks |
| 1700 | Conference Adjourned |
