Program Agenda

Visible to the public 

Submitted by Katie Dey on Tue, 02/21/2017 - 5:33pm

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

    Visible to the public 

    Submitted by willirn1 on Tue, 03/30/2021 - 10:27am

    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