| PROGRAM AGENDA | ||||
| Monday | Tuesday | Wednesday | Thursday |
Conference Timezone: EDT | |||
| MONDAY, MAY 16 Theme: Autonomous IoT |
||||
1200 - 1215 |
Welcome & Opening Remarks HCSS Chairs: Patrick Lincoln (SRI International) Lee Pike (Amazon Web Services) |
|||
| 1215 - 1315 | KEYNOTE PRESENTATION: A Navy of Things: The Role of IoT at War Roger Hallman1,2 and Megan Kline1 1Naval Information Warfare Center (NIWC) Pacific 2Thayer School of Engineering at Dartmouth |
|||
| 1315 - 1345 | High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) Joseph Kiniry (Galois, Inc.) |
|||
| 1345 - 1415 | BREAK |
|||
| 1415 - 1445 | Analyzing Code Stability Using Control Theoretic Techniques Jessa Lee (Apogee Research) |
|||
| 1445 - 1515 | Cyber Assured Systems Engineering at Scale Darren Cofer (Collins Aerospace) |
|||
| 1515 - 1545 | BREAK |
|||
| 1545 - 1630 |
MINI TALKS Correct-by-Learning Methods for Reliable Control A Method for Formal Verification of Neural Network Collision Avoidance Controller Model-checking State Machines In the Wild |
|||
| 1630 - 1700 | Machine Learning and the Unknown Unknowns Darren Cofer (Collins Aerospace) |
|||
| 1700 | Adjourn for the day |
|||
| TUESDAY, MAY 17 Themes: Cyber Defense of the Supply Chain / Identifying and Controlling Weird Machines |
||||
| 1155 - 1200 | Welcome Patrick Lincoln (SRI International) and Lee Pike (AWS) |
|||
1200 - 1300 |
KEYNOTE PRESENTATION: Limiting Weird Machines Thomas Dullien (Elastic) |
|||
| 1300 - 1330 | Tiffin and MGen: An Expressive Policy Language with Multiple Runtime Monitoring Tools Zak Fry (GrammaTech, Inc.) |
|||
| 1330 - 1345 | BREAK |
|||
| 1345 - 1415 | Model Validation for DARPA DPRIVE Ian Blumenfeld (Two Six Technologies) |
|||
| 1415 - 1500 | HCSS Formal Methods Education Panel Moderator: Perry Alexander (The University of Kansas) Panelists: Kevin Hamlen (UT Dallas) Marijn Heule (CMU) Pete Manolios (Northeastern) Yan Shoshitaishvili (Arizona State) |
|||
| 1500 - 1530 | BREAK |
|||
| 1530 - 1600 | Lifting Formal Proof to Practice via an Assurance Case Mark Thober (JHU APL) |
|||
| 1600 - 1630 |
MINI TALKS CSAADE: Cryptographically Secure, Automatic Assurance Software Development Environment Binary Software Composition Analysis with CodeSentry |
|||
| 1630 | Adjourn for the day |
|||
| WEDNESDAY, MAY 18 Theme: Driving Formal Methods to Practice I |
||||
| 1155 - 1200 | Welcome Patrick Lincoln (SRI International) and Lee Pike (AWS) |
|||
| 1200 - 1300 | Keynote: What Log4j teaches us about the Software Supply Chain Stephen Magill (Sonatype) |
|||
| 1300 - 1330 | P: Formal Modeling and Analysis of Distributed Systems Ankush Desai (Amazon) |
|||
| 1330 - 1345 | BREAK |
|||
| 1345 - 1415 | Reasoning about Deltas — Even Doing Nothing is Difficult Hira Syeda (AWS) |
|||
| 1415 - 1445 | Evolving Verified Cloud Authorization Sean McLaughlin (AWS) |
|||
| 1445 - 1530 |
MINI TALKS Applying Formal Methods to Incident Recovery Automated Evidence Generation for Continuous Certification Lowering the Barrier to Formal Modeling and Analysis |
|||
| 1530 - 1600 | BREAK |
|||
| 1600 - 1630 | Proof, but at What Cost? Robin Salkeld (AWS) |
|||
| 1630 - 1700 | Scaling Formal Verification with Specification Extraction Edwin Westbrook (Galois, Inc.) |
|||
| 1700 | Adjourn for the day | |||
| THURSDAY, MAY 19 Theme: Driving FM to Practice II |
||||
| 1155 - 1200 | Welcome Patrick Lincoln (SRI International) and Lee Pike (AWS) |
|||
1200 - 1300 |
Keynote Presentation: Supply Chain Events: Hardware vs. Software Saverio Fazzari (Booz Allen Hamilton) |
|||
| 1300 - 1330 |
Unified Configuration Modeling Infrastructure Denis Gopan (GrammaTech, Inc.) |
|||
| 1330 - 1345 | BREAK |
|||
| 1345 - 1415 | Formally Verifying Security and Compliance Mandates using AWS Network Access Analyzer Dan DaCosta (AWS) |
|||
| 1415 - 1445 | Demystify your trust boundary with interactive refinement Vaibhav Sharma (Amazon.com Services LLC) |
|||
| 1445 - 1515 | BREAK | |||
| 1515 - 1545 | Using lightweight formal methods to validate a key-value storage node in Amazon S3 James Bornholt (AWS & UT Austin) |
|||
| 1545 - 1615 | Fiat Cryptography: A Formally Verified Compiler for Finite-Field Arithmetic Adam Chlipala (MIT) |
|||
| 1615 - 1645 | Kani Rust Verifier Daniel Schwartz-Narbonne (AWS) |
|||
| 1645 - 1700 | Closing Remarks HCSS Co-Chairs: Lee Pike (AWS) and Patrick Lincoln (SRI International) |
|||
| 1700 |
Conference Adjourned | |||
| CONFERENCE ADJOURNED | ||||
Conference Archives:
2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010,
2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018, 2019, 2020,
2021