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

Implementation and verification of an SMT solver

Supervisor(s): Benedikt Ahrens, Kobe Wullaert
Posted: March 14, 2023