Interpolation-based software verification with Wolverine

Abstract

Wolverine is a software verification tool using Craig interpolation to compute invariants of ANSI-C and C++ programs. The tool is an implementation of the lazy abstraction approach, generating a reachability tree by unwinding the transition relation of the input program and annotating its nodes with interpolants representing safe states. Wolverine features a built-in interpolating decision procedure for equality logic with uninterpreted functions which provides limited support for bit-vector operations. In addition, it provides an API enabling the integration of other interpolating decision procedures, making it a valuable source of benchmarks and allowing it to take advantage of the continuous performance improvements of SMT solvers. We evaluate the performance of Wolverine by comparing it to the predicate abstraction-based verifier SatAbs on a number of verification conditions of Linux device drivers. © 2011 Springer-Verlag.