Interpolation-based Software Verification with WOLVERINE

Wolverine is a software verication 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 ofWolverine by comparing it to the predicate abstraction-based verier SatAbs on a number of verication conditions of Linux device drivers.