HCSS 2020 Program Agenda
| PROGRAM AGENDA | ||
| Monday | Tuesday | Wednesday | Thursday |
Conference Timezone: EDT | |
| MONDAY, SEPTEMBER 14 Theme: Architecture-level Formal Methods for New and Existing Systems |
||
1100 - 1145 |
PANEL: HCSS 20th Anniversary Reflections Mark Jones (Portland State University) John Launchbury (Galois) Brad Martin (NSA) Matt Wilding (Collins Aerospace) |
|
| 1145 - 1215 | Run-Time Assurance Architecture for Learning-Enabled Systems Darren Cofer (Collins Aerospace) |
|
| 1215 - 1300 | BREAK |
|
| 1300 - 1330 | KEYNOTE: IDAS: Intent-Defined Adaptive Software ARCOS: Automated Rapid Certification of Software Ray Richards (DARPA) |
|
| 1330 - 1400 | Actionable definition of Safety Design Patterns using AADLv2, ALISA and the Error Modeling Annex Jérôme Hugues (CMU/SEI) |
|
| 1400 - 1430 | BREAK |
|
| 1430 - 1530 | KEYNOTE: Take a SEAT: Security-Enhancing Architectural Transformations Konrad Slind (Collins Aerospace) |
|
| 1530 - 1600 | A Verified Optimizer for Quantum Circuits Robert Rand (University of Chicago) |
|
| 1600 - 1630 | Cryptographic Protocol Verification in AWS Adam Petcher (Amazon Web Services) |
|
| 1630 - 1700 | NETWORKING |
|
| TUESDAY, SEPTEMBER 15 Theme: Cognitive Security |
||
1100 - 1200 |
KEYNOTE: Trustworthy AI Jeannette Wing (Columbia) |
|
| 1200 - 1230 | Improving Computer Security by Understanding Cognitive Security Kimberly Ferguson-Walter (National Security Agency’s Laboratory for Advanced Cybersecurity Research) |
|
| 1230 - 1315 | BREAK |
|
| 1315 - 1400 | The Changing Face of Computational Propaganda: AI, Encryption, Geofencing and the Manipulation of Public Opinion Samuel Woolley (University of Texas, Austin) |
|
| 1400 - 1530 | POSTER & NETWORKING SESSION |
|
| WEDNESDAY, SEPTEMBER 16 Theme: Formal Methods at Scale |
||
1100 - 1200 |
PANEL: FM@Scale Workshop Summary Patrick Lincoln (SRI) Brad Martin (NSA) William Scherlis (DARPA) |
|
| 1200 - 1230 | Integration Challenges in Static Analysis and Verification Stephen Magill (MuseDev) |
|
| 1230 - 1315 | BREAK |
|
| 1315 - 1345 | Formal Verification of Production Distributed Protocols Mike Dodds (Galois) |
|
| 1345 - 1415 | Verifying C++ at Scale Gregory Malecha (BedRock Systems) |
|
| 1415 - 1445 | Analysis of the Secure Remote Password Protocol Using CPSA Erin Lanus (Virginia Tech) |
|
| 1445 - 1530 | BREAK |
|
| 1530 - 1600 | 3C: Interactive Conversion of C to Checked C Michael Hicks (Correct Computation Inc. / University of Maryland) |
|
| 1600 - 1630 | Adapting to demand: seL4 proofs and proof engineering practice Matthew Brecknell (Data61, CSIRO, Australia) |
|
| 1630 - 1700 | NETWORKING |
|
| THURSDAY, SEPTEMBER 17 Theme: Formal Methods at Scale |
||
1100 - 1200 |
KEYNOTE: Distributed and Trustworthy Automated Reasoning Marijn Heule (Carnegie Mellon University) |
|
| 1200 - 1230 | Geometric Path Enumeration Methods for Verifying ReLU Neural Networks Stanley Bak (Stony Brook University / Safe Sky Analytics) |
|
| 1230 - 1315 | BREAK |
|
| 1315 - 1345 | Verification is Engineering Joey Dodds (Galois) |
|
| 1345 - 1415 | End-to-End Verification of Initial and Transition Properties of GR(1) Designs Generated by Salty in SPARK Laura Humphrey (Air Force Research Laboratory) |
|
| 1415 - 1445 | Scalable Sound Static Analysis of Real-world C Applications using Abstract Interpretation Henny Sipma (Kestrel Technology) Paul E. Black (NIST) |
|
| 1445 - 1530 | BREAK |
|
| 1530 - 1600 | Automated Analysis of AWS Access Control Andrew Gacek (Amazon Web Services) |
|
| 1600 - 1630 | Code-Level Model Checking in the Software Development Workflow Daniel Schwartz-Narbonne (Amazon Web Services) |
|
| 1630 - 1700 | NETWORKING |
|
| CONFERENCE ADJOURNED | ||
