Algorithmic Logic-based Verification

Developing an automated program verifier is an extremely difficult task. By its very nature, a verifier shares many of the complexities of an optimizing compiler and of an efficient automated theorem prover. From the compiler perspective, the issues include idiomatic syntax, parsing, intermediate representation, static analysis, and equivalence preserving program transformations. From the theorem proving perspective, the issues include verification logic, verification condition generation, synthesizes of sufficient inductive invariants, deciding satisfiability, interpolation, and consequence generation. Luckily, the cores of both compilers and theorem provers are well understood, well-defined, and readily available. In these lectures, we examine how to build a state-of-the-art program verifier by re-using much of existing compilers and SMT-solvers. The lectures are based on the SeaHorn verification framework developed in collaboration between University of Waterloo and SRI International.