Program Agenda
The HCSS Conference will be held May 6-8, 2024.
The co-located Software Certification Consortium (SCC) Meeting and the Trusted Computing Center of Excellence (TCCoE) Summit will be held May 9-10.
Download the TCCoE Summit agenda
View the SCC Meeting agenda
| PROGRAM AGENDA | ||
| Monday | Tuesday | Wednesday |
||
| MONDAY, MAY 6 Theme: Use of Large Language Models in High-Assurance Contexts |
||
| 0900 - 1000 | KEYNOTE Can Computers Beat Humans at Design? Wojciech Matusik (MIT) |
|
| 1000 - 1030 | BREAK | |
| 1030 - 1100 | Small, reliable ways to use LLMs: macro refolding, proof writing, and protocol modeling Mike Dodds (Galois, Inc.) |
|
| 1100 - 1130 | Metrics for Large Language Model-Generated Proofs in a High-Assurance Application Domain Amer Tahat and David Hardin (Collins Aerospace) |
|
| 1130 - 1200 | Towards Creative Generative Models for Scientific Discovery Susmit Jha (SRI) |
|
| 1200 - 1330 | LUNCH (on your own) | |
| 1330 - 1400 | Automated Theory Substitution: Toward Proof-Driven Software Development John Scebold and Jared Ziegler (Two Six Technologies) |
|
| 1400 - 1430 | AI-enabled Rapid Intelligent Systems Engineering Mauricio Castillo-Effen (Lockheed Martin) |
|
| 1430 - 1500 | AI for Rigorous Digital Engineering Joseph Kiniry (Galois, Inc.) |
|
| 1500 - 1530 | Poster Session / Break | |
| 1530 - 1600 | Logic Augmented Generative Models For High-Assurance Applications Sumit Jha (Florida International University) |
|
| 1600 - 1630 | Clover: Closed-Loop Verifiable Code Generation Chuyue Sun and Ying Sheng (Stanford University) |
|
| 1630 - 1700 | Property-Driven Continuous Assurance of Software Designs Srivatsan Varadarajan (Honeywell Aerospace) |
|
| 1700 | Adjourn for the day |
|
| TUESDAY, MAY 7 Theme: Assured Open Source and Memory Safety |
||
| 0900 - 1000 | KEYNOTE CHERI: Architectural Support for Memory Protection and Software Compartmentalization Robert Watson (University of Cambridge) |
|
| 1000 - 1030 | BREAK | |
| 1030 - 1100 | Formal Verification of AWS-LibCrypto Yan Peng (Amazon Web Services) |
|
| 1100 - 1130 | ARBITER & UPSAT: Assuring Open Source Software Howard Reubenstein and Greg Eakman (STR) |
|
| 1130 - 1200 | Zero Trust Design and Assurance Patterns for Cyber-Physical Systems Saqib Hasan, Isaac Amundson, and David Hardin (Collins Aerospace) |
|
| 1200 - 1330 | LUNCH (on your own) |
|
| 1330 - 1430 | KEYNOTE Fireside Chat with Josh Baron (National Security Council, The White House) |
|
| 1430 - 1500 | Industrial Scale Proof Engineering for Critical Trustworthy Applications (INSPECTA) Darren Cofer (Collins Aerospace) |
|
| 1500 - 1530 | BREAK | |
| 1530 - 1600 | An Assured Open Source Framework for Runtime Verification Alwyn Goodloe (NASA Langley Research Center), Ivan Perez (NASA Ames), and Ryan Scott (Galois, Inc.) |
|
| 1600 - 1630 | High-Assurance Synthesis and Analysis Techniques for Memory-Safe Programming Languages David Hardin (Collins Aerospace) |
|
| 1630 - 1700 | Developing and Maintaining the Assurance of Software with Open-Source Components: Challenges and Tools Gabor Karsai (Vanderbilt University) |
|
| 1700 | Adjourn for the day |
|
| 1830 | HCSS Conference Dinner Chart House Prime | 300 Second St, Annapolis, MD 21403 |
|
| WEDNESDAY, MAY 8 Theme: Program Transformations |
||
| 0900 - 1000 | KEYNOTE Automatic Program Transformation Claire Le Goues (CMU) |
|
| 1000 - 1030 | BREAK | |
| 1030 - 1100 | Correct-by-construction Cryptographic Hardware via Explicit Staging Transformations William Harrison and Yakir Forman (Two Six Technologies) |
|
| 1100 - 1130 | Optim(L): Generating Lazy APIs from DAGs of Actions Mark Tullsen (Galois, Inc.) |
|
| 1130 - 1200 | Assuring Transformative Technologies Robin Bloomfield (Adelard (NCC Group) and City, University of London) |
|
| 1200 - 1330 | LUNCH (on your own) |
|
| 1330 - 1400 | Putting a Roof Over Your Head: Object-Oriented Programming in Rust Thomas Wahl (GrammaTech, Inc.) |
|
| 1400 - 1430 | Formally Verifying the Rust Standard Library with Verus Bryan Parno (Carnegie Mellon University) |
|
| 1430 - 1500 | Practical Software Supply Chain Assurance Leonardo Babun and Kathleen N. McGill (Johns Hopkins Applied Physics Laboratory) |
|
| 1500 - 1530 | Sponsored Break | |
| 1530 - 1600 | Reverse Architecting Software Binaries Greg Nelson and Denis Gopan (GrammaTech Inc.) |
|
| 1600 - 1630 |
TCCoE & S&CC Introductions HCSS Closing Remarks |
|
| 1630 | Conference Adjourned | |
