HCSS 2021 Program Agenda

 

PROGRAM AGENDA
Monday | Tuesday | Wednesday | Thursday Conference Timezone: (EDT)
MONDAY, MAY 3    
Theme: Proof Robustness: decade-long experiences | Chair: Matt Wilding

1315 - 1330
Welcome & Opening Remarks    
HCSS Chairs:    
June Andronick (Proofcraft & UNSW Sydney)    
Lee Pike (Amazon Web Services)    
 
1330 - 1430 KEYNOTE: Robustness of formal verification of x86 microprocessors    
Anna Slobodova (Centaur)    
 
1430 - 1500 Proof Robustness in ACL2    
Eric Smith (Kestrel Institute)    
 
1500 - 1530 BREAK    
 
1530 - 1600 How to Improve the Robustness of Auto-active Program Proof Through Redundancy    
Yannick Moy (AdaCore)    
 
1600 - 1630 Proof Robustness in the seL4 Verification    
Gerwin Klein (Proofcraft & UNSW Sydney) and Rafal Kolanski (Proofcraft & seL4 Foundation)    
 
1630 - 1645 BREAK + FIRESIDE + CLOSING REMARKS FROM SESSION CHAIR    
 
   
TUESDAY, MAY 4    
Theme: Holistic System Reasoning | Chair: John Launchbury

1330 - 1430
KEYNOTE: Mitigating Emergent Computation: the need for new approaches in systems engineering    
Sergey Bratus (DARPA)    
 
1430 - 1500 Compositional verification of modular C programs using VST and VSU     
Lennart Beringer (Princeton University)    

Formalizing and Evaluating Checked C    
Michael Hicks (University of Maryland)    

On Computing Relevant Parameters of Decision Functions    
Susmit Jha (SRI International)    
 
1500 - 1515 Lightning Talk Fireside    
 
1515 - 1530 BREAK    
 
1530 - 1600 Knowledge-Assisted Reasoning of Model-Augmented System Requirements    
Brendan Hall (Honeywell Advanced Technology)    
 
1600 - 1630 Safe Composition through Dynamic Feature Interaction Resolution    
Eunsuk Kang (CMU)    
 
1630 - 1645 BREAK    
 
1645 - 1715 Automating Argumentation (for Overarching Properties) with Goal-directed Answer Set Programming    
Gopal Gupta (UT Dallas)    
 
1715 - 1730 BREAK + FIRESIDE + CLOSING REMARKS FROM SESSION CHAIR    
 
   
WEDNESDAY, MAY 5    
Theme: Morning: Formal Methods in DevOps | Chair: Brad Martin    
             Afternoon: Reasoning About Security, Crypto, & Protocols | Chair: Perry Alexander

1330 - 1400
Retrofitting a type system onto a real world dynamic expression language    
Vaibhav Sharma & Bilal Khan (AWS)    
 
1400 - 1500 KEYNOTE: DoD Enterprise DevSecOps Initiative & Platform One    
Nicolas Chaillan (USAF)    
 
1500 - 1515 BREAK    
 
1515 - 1545 Continuous Integration and Formal Methods with Muse, Affix, and 5C    
Stephen Magill (MuseDev / Sonatype) and Michael Hicks (University of Maryland)
1545 - 1615 BREAK + FIRESIDE    
 
1615 - 1645 Automated Trust Analysis for Layered Attestations    
Ian Kretz (MITRE)    
 
1645 - 1715 CYBORG Cryptographic Security: Bluetooth, Signal, and Beyond    
Britta Hale (NPS)    
 
1715 - 1745 Zero-knowledge Proofs of Binary Exploitability    
Ben Perez (Trail of Bits)    
 
1745 - 1800 BREAK + FIRESIDE + CLOSING REMARKS FROM SESSION CHAIR    
 
   
THURSDAY, MAY 6    
Theme: Exploring Compositionality | Chair: Ray Richards

1330 - 1430
KEYNOTE: Enabling Provable Security at Scale    
Neha Rungta (AWS)     
 
1430 - 1500    
 		 Briefcase Full of Proofs    
Darren Cofer (Collins Aerospace)    
 
1500 - 1530 BREAK    
 
1530 - 1600 HAMR - High-Assurance Modeling and Rapid Engineering for Embedded Systems Using AADL    
John Hatcliff (Kansas State University)    
 
1600 - 1630 Verifiable Binary Lifting    
Joe Hendrix (Galois)    
 
1630 - 1645    
 		 BREAK + FIRESIDE + CLOSING REMARKS FROM SESSION CHAIR
   
CONFERENCE ADJOURNED