Case study in automated theorem proving
Master Project

Project Description

In this project, you develop a case study in the use of automated theorem provers.

The subject domain, that is, the area of reasoning that you want to work in, is your choice: this could be in the area of mathematics, program verification, or other.

Some automated theorem provers are described in these bachelor theses:

• Why3
• Dafny
• KeY
• SPARK
• Vampire

Project Goals

In this project, you will work on the following goals:

• Learn the basics of automated theorem proving: decision procedures, heuristics, etc.
• Learn to use one or more automated theorem provers
• Learn a subject domain well enough to formulate theorems in it.

Contacts for the Project

• Benedikt Ahrens (TU Delft)