2020 Program Agenda

EDT

TIME ZONE

MON, SEPT 14

Arch. Level FM

TUES, SEPT 15

Cognitive Security

WED, SEPT 16

FM@Scale

THUR, SEPT 17

FM@Scale
1100 - 1145

PANEL



HCSS 20th Anniversary Reflections

 

KEYNOTE 



Trustworthy AI

Jeannette Wing

(Columbia)

PANEL



FM@Scale Workshop Summary

Patrick Lincoln (SRI)

William Martin (DoD)

William Scherlis (DARPA)

KEYNOTE 



Distributed and Trustworthy Automated Reasoning 

Marijn Heule

(Carnegie Mellon University)
1145 - 1200

Run-Time Assurance Architecture for Learning-Enabled Systems

Darren Cofer

(Collins Aerospace)
1200 - 1215

 

Kim Ferguson-Walter

(DoD)

Integration Challenges in Static Analysis and Verification

Stephen Magill

(MuseDev)

Geometric Path Enumeration Methods for Verification of Neural Networks

Stanley Bak

(Stony Brook University

/ Safe Sky Analytics)
1215 - 1230 BREAK
1230 - 1245

BREAK

BREAK

BREAK
1245 - 1300
1300 - 1315

KEYNOTE

Philomena Zimmerman

(Office of the Under Secretary of Defense for Research and Engineering)
1315 - 1330

David Burke

(Galois)

 

Formal Verification of Production Distributed Protocols

Mike Dodds

(Galois)

 Scaling Continuous Verification of Cryptography

Joey Dodds

(Galois)
1330 - 1345 Actionable definition of Safety Design Patterns using AADLv2, ALISA and the Error Modeling Annex

Jerome Hugues

(CMU/SEI)
1345 - 1400

Verifying C++ at Scale

Gregory Malecha

(BedRock Systems)

End-to-End Verification of Initial and Transition Properties of GR(1) Designs Generated by Salty in SPARK

Laura Humphrey

(Air Force Research Laboratory)
1400 - 1415 BREAK TBA
1415 - 1430 Analysis of the Secure Remote Password Protocol Using CPSA

Alan Sherman

(UMBC)		 Scalable Sound Static Analysis of Real-world C Applications using Abstract Interpretation

Henny Sipma

(Kestrel Technology)
1430 - 1445





KEYNOTE

Architecture-Level FM

Konrad Slind

(Collins Aerospace)





 
1445 - 1500 BREAK BREAK BREAK
1500 - 1515
1515 - 1530
1530 - 1545 A Verified Optimizer for Quantum Circuits

Robert Rand

(University of Maryland)

POSTER SESSION

 

 Interactive Conversion of C to Checked C

Mike Hicks

(Correct Computation Inc. / University of Maryland)

One-click Automated Reasoning in Amazon Web Services

Andrew Gacek

(Amazon Web Services)
1545 - 1600
1600 - 1615 Cryptographic Protocol Verification in AWS

Adam Petcher

(Amazon Web Services)

Adapting to demand: seL4 proofs and proof engineering practice

Matthew Brecknell

(Data61, CSIRO, Australia)

 Code-Level Model Checking in the Software Development Workflow

Daniel Schwartz-Narbonne

(Amazon)
1615 - 1630
1630 - 1645 Networking Networking Networking Networking
1645 - 1700