Program reasoning has important and wide-ranging applications in programming languages, such as type inference, static analysis, testing, verification, and synthesis. This tutorial will cover how to build program reasoning tools using two versatile, modern, and open-source systems: the LLVM compiler infrastructure and the Z3 constraint solver. These systems underlie state-of-the-art tools such as Clang Static Analyzer, the KLEE symbolic execution engine, and the SeaHorn verification framework.

This tutorial will introduce LLVM and Z3’s architecture and conduct three hands-on exercises. The exercises will target common applications in program reasoning that embody three distinctive use-cases: static dataflow analysis, dynamic symbolic execution, and assertion verification. The target audience for this tutorial is those who want hands-on experience with state-of-the-art tools and techniques employed in program reasoning. The tutorial presumes background in C++ programming and basic logical reasoning.