All events will be held virtually. Times listed are Eastern Standard Time.

Day 1 (Wed, Feb. 3)

8:45 AM - 9:00 AM Opening Remarks

Tutorial 1: The Z3 Theorem Prover (9:00 AM - 12:00 PM)

Phil Zucker, Draper Labs
(20 min coffee break from 10:10AM-10:30AM)
[Tutorial Notebook]

12:00 PM - 1:00PM: Social Hour

Day 2 (Thurs, Feb. 4)

8:45 AM - 9:00 AM Opening Remarks

Tutorial 2: The Coq Theorem Prover (9:00 AM - 12:00 PM)

Cody Roux, Draper Labs
(20 min coffee break from 10:10AM-10:30AM)
[Tutorial Problems] [Tutorial Solutions]

12:00 PM - 1:00PM: Social Hour

Day 3 (Fri, Feb. 5)

8:45 AM - 9:00 AM Opening Remarks

Session 1: General Topics

Keynote: Kathleen Fisher, Tufts University (9:00 AM - 9:50 AM)
Using Formal Methods to Eliminate Exploitable Bugs [slides]

9:55 AM - 10:05 AM: Break

Session 2: Verified Software Components

Gregory Malecha, BedRock Systems (10:05 AM - 10:30 AM)
Bringing Verification to the Mainstream: Verifying Concurrent C++ [slides]

Session 3: Distributed Systems

Hillel Wayne, Windy Coast Consulting (10:35 AM - 11:00 AM)
Designing Distributed Systems with TLA+ [slides]

11:00 AM - 11:10 AM: Break

Session 4: Robust Machine Learning

Mathew Mirman, ETH Zurich (11:10 AM - 11:35 AM)
Safe Deep Learning [slides]

Closing Remarks and Social Hour (11:40 AM - 1:00 PM)