Implementation and verification of an SMT solver
Master Project

Project Description

An SMT solver is a similar to a SAT solver. However, instead of having atomic boolean variables at the leaves of formulas, an SMT solver considers formulas whose leaves are given by domain-specific formulas such as x < 5, 3x + 2y - z >= 0, f(x) = 0, or forall x, y, g(x,y) = z.

Many computer proof assistants communicate with SMT solvers, by translating a proof goal into a suitable formula, passing it to the SMT solver, and receiving the result.

In this project, you will implement and verify an SMT solver within a computer proof assistant.

Project Goals

In this project, you will work on (some of) the following goals:

• Learn to use one or more computer proof assistants, e.g., Coq, Agda, Lean, Isabelle
• Understand how an SMT solver works
• Implement an SMT solver in a computer proof assistant
• State and prove desirable properties of the SMT solver (soundness, completeness, other properties depending on the domains where the leaf formulas come from)

Contacts for the Project

• Benedikt Ahrens (TU Delft)
• Kobe Wullaert (TU Delft)