Program Agenda
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 Robustness, Exploring 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:
2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010,
2011, 2012, 2013, 2014, 2015, 2016, 2017, 2018, 2019, 2020
Monday | Tuesday | Wednesday | Thursday |
Conference Timezone: Eastern Daylight Time (EDT) PRINT-FRIENDLY VERSION |
||
![]() |
|||
MONDAY, MAY 3 Theme: Proof Robustness: decade-long experiences | Chair: Matt Wilding |
|||
1315 - 1330 |
Welcome & Opening Remarks |
||
1330 - 1430 | KEYNOTE PRESENTATION 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 (CSIRO / UNSW, Sydney) |
||
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, Implementing, and Evaluating Null-Terminated Arrays in 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 Brenden 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 (AWS) |
||
1400 - 1430 | Continuous Integration and Formal Methods with Muse, Affix, and 5C Stephen Magill (MuseDev / Sonatype) and Michael Hicks (University of Maryland) |
||
1430 - 1500 | BREAK |
||
1500 - 1600 | KEYNOTE PRESENTATION TBA |
||
1600 - 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: 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 |