HCSS 2021 Program Agenda
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 | |||
