Analyzing Programs with Z3

Tikhon Jelvis demonstrates how to compile a simple imperative language to SMT formulas and verify program invariants using the Z3 solver.

Tikhon Jelvis C◦mp◦se :: Conference composeconference.org/ February 5, 2016 SMT solvers are widely used in research to analyze and verify programs. This lets us check invariants and compare programs against a spec exhaustively, with bounds on the number of loop iterations and the size of the heap. SMT solvers are also useful for other sorts of analysis including sophisticated type checking (like refinement types in Liquid Haskell) and fields other than program analysis (like security research where they can be used to analyze cryptographic algorithms and protocols). I’ll demonstrate how to compile a simple language to an SMT formula and analyze programs using the Haskell Z3 bindings. Z3 has bindings in other languages including OCaml and .NET, so these ideas will be immediately useful to everyone even if the details are slightly different from the Haskell code. The underlying ideas will also help people approach other problems with Z3.