Links on Modern Automated Provers and Constraint Solvers
SAT background (practical considerations)
- An Extensible SAT-solver (original MiniSat implementation description)
SMT (Satisfiability Modulo Theories)
- Theorem Proving using Lazy Proof Explication and the corresponding Slides on Lazy Proof Explication
Finite Model Finding
- Calculi for Program Incorrectness and Arithmetic, Philipp Rümmer's PhD thesis