Analyzing Programs with Z3

Tikhon Jelvis
C◦mp◦se :: Conference
http://www.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.