Analyzing Programs with SMT Solvers

We can use SMT solvers like Z3 to analyze programs and answer difficult questions about our code. By generating and solving complex constraints, we can improve error message localization, attack cryptographic protocols, check refinement types, search for proofs, verify invariants, compare programs against specifications or even synthesize code. Z3 is the goto state-of-the-art SMT solver, available under and open source license and has a first-class OCaml library.

In this talk, I'll walk through a simple OCaml program to generate SMT constraints that represent a bounded model of programs in a simple imperative language. Algebraic data types and pattern matching are a perfect fit for this kin