Program Agenda

Visible to the public 

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 
Sicun Gao (UCSD)

A Method for Formal Verification of Neural Network Collision Avoidance Controller 
Daniel Genin (JHU APL)

Model-checking State Machines In the Wild 
Vaibhav Sharma (Amazon.com Services LLC)

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 
Leonardo Babun (JHU APL)

Binary Software Composition Analysis with CodeSentry 
Antonio Flores Montoya (GrammaTech, Inc.)

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 
Aleksandar Chakarov (AWS Identity)

Automated Evidence Generation for Continuous Certification 
Mauricio Castillo-Effen (Lockheed Martin Advanced Technology Laboratories)

Lowering the Barrier to Formal Modeling and Analysis 
Daniel Balasubramanian (VU-ISIS)

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:
2001200220032004200520062007200820092010
201120122013, 2014, 2015, 2016, 2017, 2018, 2019, 2020,
2021