Proof Automation

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.

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.

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