Philippe Suter, Ali Sinan Köksal, and Viktor Kuncak. Satisfiability modulo recursive programs. In Static Analysis Symposium (SAS), 2011.

We present a semi-decision procedure for checking expressive correctness properties of recursive first-order functional programs. In our approach, both properties and programs are expressed in the same language, which is a subset of Scala. We have implemented our procedure and integrated it with the Z3 SMT solver and the Scala compiler. Our procedure is sound for proofs and counterexamples. It is terminating and thus complete for many important classes of specifications, including 1) all verification problems containing counterexamples, 2) functions annotated with inductive postconditions, and 3) abstraction functions and invariants of recursive data types that commonly arise in functional programs. Using our system, we verified detailed correctness properties for functional data structure implementations, as well as Scala syntax tree manipulations. We have found our system to be fast for both finding counterexamples and finding correctness proofs, and to scale to larger programs than alternative techniques.

[ bib ] Back