We have two 90 minute lectures (which will be split into two 45 minute-ish halves). We'll cover:
- intro to propositional SAT
- how to use SAT solvers
- some examples of using SAT solvers (inc. via CBMC)
- intro to SMT
- how to use SMT solvers
- application of SMT solving: Amazon Zelkova
- application of SMT solving: Synthesis
- using UCLID5 to generate SAT/SMT models
I'll be using the following tools:
- Day 1+2: The Z3 SMT solver (which also allows you to use its internal SAT solver directly)
- Day 1: CBMC - a bounded model checker for C programs
- Day 2: UCLID5 - a modeling and verification tool that interfaces with SMT solvers
- Day 2: CVC5 - an SMT solver and synthesis solver
I'm not using them, but the following tools are worth a mention:
- MiniSAT: a really simple SAT solver
- RISS: a SAT solver good at incremental SAT solving and parallel SAT solving
- DReal: an SMT solver specialising in real arithmetic
- BitWuzla: An SMT solver specialising in bitvectors and floating point arithmetic
All the examples from the slides are in the examples directory, except Example 4, which is too large, and example 7 which is Amazon's Zelkova
- Example 1: checking equivalence of code
- Example 2: professorial room allocation
- Example 3: simple CBMC example
- Example 4: CBMC for Xen
- Example 5: simple SMT
- Example 6: Sudoku (with various encodings)
- Example 7: Zelkova
- Example 8: Invariants
- Example 9: UCLID5 examples
File extensions tell you which tool you can use to run the file:
name.c
is a C file. Runcbmc name.c --trace
name.smt2
can be run with Z3 or CVC5. Runz3 name.smt2
name.dimacs
can be run with Z3name.sl
is a synthesis file, run with CVC5name.ucl
is a UCLID5 file, runuclid5 name.ucl