About the Class

What will it take to build a world in which programmers of all skill levels can formally prove the absence of costly or dangerous bugs in software systems? This seminar will explore technologies for automating formal proofs about software systems in proof assistants like Coq, Lean, or Isabelle/HOL.

Example topics include languages for proof automation, automated theorem proving for proof assistants, plugins and transformations, neural proof synthesis, and usable automation. These topics will be explored through a combination of paper reading and collaborative exploration of code artifacts.

Background in functional programming is expected; background in proof assistants is not needed.

Format

Class Format

The class will meet twice per week. Every one or two week period will explore a particular topic in proof automation. In a typical week, on the first day, we will discuss a paper related to that topic in depth. On the second day, we will collaboratively explore and modify a code artifact associated with that paper. The goal of this format is to really give students a sense of how proof automation works, demystifying what can at times feel like magic.

Some weeks may feature guest lectures in lieu of paper discussions or artifact explorations. The final week will center project proposals by students in the class, with the goal of fostering collaboration.

As this is a graduate special topics seminar, grading will be based on just showing some basic effort. Students will each be expected to facilitate one paper discussion with me---this basically just means reading the paper in more depth than other papers, showing up with additional discussion questions, and keeping the conversation going. There will also be very small (less than one paragraph) discussion exercises for each paper and artifact on a class forum. And there will be a project proposal during the last week. The goal is just to learn some cool new things and inspire some cool new projects.

Schedule

Class Schedule

The schedule below is an early outline, and is subject to change. Unpopulated links will be populated soon.

Topic Day 1 Day 2
Getting Started
Impacts & Ethics

This week is asynchronous due to POPL.
01/18/2022
Async

Watch
Read
Discuss
01/20/2022
Async

Watch
Read
Discuss
Getting Started
Foundations

Sign up to facilitate discussions in future weeks!
01/25/2022
11:00 AM

Read
Discuss
Sign Up
01/27/2022
11:00 AM

Install
Hack
Languages
Tactics & More
02/01/2022
11:00 AM

Read
Discuss
02/03/2022
11:00 AM

Install
Hack
Languages
Logics & Reflection
02/08/2022
11:00 AM

Read
Discuss
02/10/2022
11:00 AM

Install
Hack
Customization
Custom Tactics
02/15/2022
11:00 AM

Read
Discuss
02/17/2022
11:00 AM

Install
Hack
Customization
Proof Procedures
02/22/2022
11:00 AM

Read
Discuss
02/24/2022
11:00 AM

Install
Hack
Plugins
Mixed Methods

Guest: Leonidas Lampropoulos (Maryland)
03/01/2022
11:00 AM

Read
Ask
03/03/2022
11:00 AM

Install
Hack
Plugins
Proof Repair
03/08/2022
11:00 AM

Read
Discuss
03/10/2022
11:00 AM

Install
Hack
Spring Break
Rest
03/15/2022
No Class
03/17/2022
No Class
ATP for ITP
E-Graphs
03/22/2022
11:00 AM

Read
Discuss
03/24/2022
11:00 AM

Install
Hack
ATP for ITP
Hammers
03/29/2022
11:00 AM

Read
Discuss
03/31/2022
11:00 AM

Install
Hack
Neural Synthesis
Tactic Prediction
04/05/2022
11:00 AM

Read
Discuss
04/07/2022
11:00 AM

Install
Hack
Neural Synthesis
Autoformalization

Guests: Christian Szegedy (Google) and Stanislas Polu (OpenAI)
04/12/2022
11:00 AM

Skim
Ask
04/14/2022
11:00 AM

Install
Hack
Human Factors
User Studies
04/19/2022
11:00 AM

Read
Discuss
04/21/2022
11:00 AM

Install
Hack
Human Factors
Social Processes

Get started on your project pitches for next week!
04/26/2022
11:00 AM

Read
Discuss
04/28/2022
11:00 AM

Write
Discuss
What's Next?
Project Pitches

Pitch your ideas and form interest-based teams for the final proposal.
05/03/2022
11:00 AM

Write
Pitch
Discuss
05/05/2022
11:00 AM

Team Up
Discuss
What's Next?
Finals Week

Final proposals are due Thursday.
05/10/2022
No Class
05/12/2022
No Class

Submit