Course syllabus


Summary

Automated theorem provers are tools that determine, automatically or with human assistance, the validity of formulas in a given logic. This course will focus on hot topics in automated theorem proving and automated deduction techniques, with an eye on how to use automated theorem provers, automated deduction techniques, program analysis techniques, or a combination of these, to prove useful properties of software systems. The course will cover various theorem provers, theorem-proving techniques, and program-analysis techniques, with a focus on what properties and/or limitations of these theorem provers and techniques make them appropriate or inappropriate for certain tasks. More broadly, the course will be concerned with how we can automatically reason about software systems, and how automated theorem proving techniques fit into this bigger picture.

The format of the course will be a combination of lectures, discussions, and student presentations. The course will be available in three options:

I strongly encourage you to take the 4 credit option, since the class project will be one of the most exciting parts of the class.

Detailed course description

Automated theorem provers have been around since the 60s and they have been put to use in many applications. They have been used to solve open problems in mathematics, but more importantly for our purposes, they have been used to prove interesting properties about real-world systems, properties that would have been hard, difficult or tedious to prove by hand. For example, automated theorem provers have been used to verify microprocessors, communication protocols, concurrent algorithms, and various properties of software systems.

In this course, we will explore the area of automated theorem proving, with an eye towards using them for practical purposes. We will look at recent novel uses of theorem provers in the research literature, and try to understand the key insights that made them succeed. We will also learn how to go about solving a problem with a theorem prover. In particular, some of the questions we will explore include: How should a given problem be encoded in formal logic, so that a theorem prover can understand it? What theorem provers, theorem-proving techniques, or program-analysis techniques would be a good match for a given problem? How can one engineer proofs so that the theorem prover will be able to perform them automatically? How can one use failed proof attempts productively?

To answer these questions, we will learn about various theorem provers and various theorem-proving and program-analysis techniques, focusing on comparing them to one another, and understanding how their limitations affect their applicability. At the same time, learning about theorem proving techniques will allow us to understand how these techniques can be applied outside of the domain of theorem proving, in the broader context of reasoning about software systems.

Course topics are flexible, but a tentative list would include:

Course project

The course project will allow you to get some hands-on experience with some theorem provers. There will be two parts to the project:

  1. A mini-project, due about 3 weeks into the class. In this part, you will be given a very simple problem, and you will encode this problem in various theorem provers. The goal of this part will be to gain familiarity with several theorem provers, and to understand the various tradeoffs between these theorem provers.
     
  2. The project per se, in which you will use a theorem prover to prove some properties of a system or part of the system. A project proposal will be due a few weeks into the class, and there will be several milestones along the way, to make sure that you are making good progress. A project report will be due at the end of the quarter.