All events will be held in the Yellowstone conference room on the 2nd floor of the Broad Institute at 415 Main St Cambridge, MA.

Day 1

8:00 AM - 8:45 AM Breakfast and Registration
8:45 AM - 9:00 AM Opening Remarks

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

Phil Zucker, Draper Labs
(30 min coffee break from 10:00AM-10:30AM)

12:00 PM - 1:00 PM Lunch

[Lunch will not be provided on the first day, but please see this map of the many local eateries just a short walk from the Broad in the Kendall Square. Food can also be purchased from the Fooda stand just outside the conference room on the 2nd floor of the Broad.]

1:00 PM - 1:45 PM Tour of Broad Genomics Platform

Tutorial 2: The Coq Theorem Prover (2:00 PM - 5:00 PM)

Cody Roux, Draper Labs
(30 min coffee break from 3:00PM-3:30PM)

Day 2

8:00 AM - 8:45 AM Breakfast and Registration
8:45 AM - 9:00 AM Opening Remarks

Session 1: General Topics

Adam Chilpala, MIT CSAIL (9:00 AM - 9:25 AM)
Mechanized Proofs of Secure and Open-Source Embedded Systems

James Koppel, MIT CSAIL (9:25 AM - 9:50 AM)
Why Haven’t PL/FM Tools Taken Over the World?

Keynote: Kathleen Fisher, Tufts University (9:50 AM - 10:40 AM)
Using Formal Methods to Eliminate Exploitable Bugs

10:40 AM - 10:50 AM: Message from Sponsors

10:50 AM - 11:10 AM: Coffee Break

Session 2: Verified Software Components

Gregory Malecha, BedRock Systems (11:10 AM - 11:35 AM)
Bringing Verification to the Mainstream: Verifying Concurrent C++

Joseph Tassarotti, Boston College (11:35 AM - 12:00 PM)
Verifying Concurrent, Crash-Safe Systems with Perennial

12:00 PM - 1:00 PM: Lunch (provided)

Session 3: Distributed Systems

Hillel Wayne, Windy Coast Consulting (1:00 PM - 1:25 PM)
Designing Distributed Systems with TLA+

Keynote: John Harrison, Amazon Web Services (1:25 PM - 2:15 PM)
Adventures in Verifying Arithmetic

2:15 PM - 2:45 PM: Coffee Break

Session 4: Robust Machine Learning

Michael Carbin, MIT CSAIL (2:45 PM - 3:10 PM)
Engineering Approximate Computations

Nathan Fulton, MIT-IBM Watson AI Laboratories (3:10 PM - 3:35 PM)
A Formal Methods Perspective on Safe Reinforcement Learning

Mathew Mirman, ETH Zurich (3:35 PM - 4:00 PM)
Safe Deep Learning

Closing Remarks (4:00 PM - 4:15 PM)