Labs
Lab 1
In this lab, you need to use MiniSat to solve a real problem. MiniSat is a minimalistic, open-source SAT solver and provides many useful programming interface. You need to convert a real problem to a proposition logic formula and use MiniSat to solve the formula.
Lab 2
In this lab, you need to implement a symbolic execution engine called MiniSEE and use it to formally verify C programs. MiniSEE converts the correctness of programs to first-order logic formulas and uses Z3, a well-known SMT solver, to solve the formulas.
Lab 3
In this lab, you need to use Dafny to formally verify real programs. Dafny is an imperative and functional compiled language and is widely used in formal verification.
Bonus Lab
In this lab, your goal is to optimize the performance of a CDCL (Conflict-driven Clause learning) SAT solver.
You can find detailed information about the CDCL approach in a note from Tommi Junttila. The solver provided in this lab follows the CDCL approach, introducing much more sophisticated techniques to improve the performance of the solver, and is modularized to allow for easy extension. Detailed information about the bonus lab, as long as the instructions for the lab, can be found in the website.