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:

- a low-credit option (1 credit), where you will only have to attend
class, and participate in discussions. This will be graded S/U.

- a medium-credit option (2 credits), where you will also have to
read the papers, and write short paper reviews. This will be graded
S/U.

- a high-credit option (4 credits), where you will also work on a course project. The course project will involve using a theorem prover to automatically prove certain properties of a system or part of a system that you are interested in. For example, you could use a theorem prover to prove properties of network protocols, of security policies, of rule based systems, of database components, or of operating system components. The goal of the project is not to reproduce previous work, or to closely mimic previous work, but rather to try something new, and explore the issues that arise in doing so. The high-credit option will be graded with a letter grade.

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:- Interesting and novel uses of theorem provers, automated deduction techniques, or program analysis techniques
- Logics and formal encodings of problems
- Basic search strategies:
- searching in the proof space domain
- searching in the semantic domain
- tactics and tacticals

- Handling various aspects of first-order logic automatically, for
example:
- quantifiers
- equality
- recursion

- Decidability and decision procedures
- decidable subsets of first-order logic
- communication between decision procedures
- communication between the theorem prover and decision procedures

- Counter-examples
- using counter-examples productively
- counter-example driven refinement

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

- 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.

- 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.