##
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)

Implementation and verification of an SMT solver

Supervisor(s): Benedikt Ahrens, Kobe Wullaert

Posted: March 14, 2023