Program Agenda

Visible to the public 

CONFERENCE
May 3-6, 2021 (virtual)
The conference program will feature invited speakers, panel discussions, and a technical track of contributed talks. The daily themes for 2021 are Proof RobustnessExploring Composability, and Continuous Development & Formal Methods.

The conference is four days this year instead of the usual three. This allows for shorter days to help combat screen fatigue and also accommodate time zone differences. The conference schedule will adhere to the Eastern Daylight Timezone (EDT). The Hopin virtual conference platform will be used to host the conference. The conference is free to attend, but you must register. For an introduction to the virtual platform please visit the Virtual Venue page.

Conference Archives:
2001200220032004200520062007200820092010
201120122013, 2014, 2015, 2016, 2017, 2018, 2019, 2020

Visible to the public 


Monday | Tuesday | Wednesday | Thursday
Conference Timezone: Eastern Daylight Time (EDT)
PRINT-FRIENDLY VERSIONs: EDT | PDT | AEST
 
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