Interpolation-based Model Checking

Wolverine

About Wolverine

Wolverine is an interpolation-based software verification tool for ANSI-C and C++ programs and aims at computing Hoare-style correctness proofs for software programs. The tool is an implementation of the lazy abstraction with interpolants algorithm.

Features

Wolverine supports checking of reachability properties such as

  • assertions
  • buffer overflows
  • pointer-safety
  • division-by-zero
  • arithmetic underflow and overflow
  • reachability of user-specified program locations
If the program analysis succeeds, the tool provides either a counterexample to the claim or a Hoare-proof and program invariants establishing the (partial) correctness of the program.

Moreover, Wolverine provides

  • a built-in interpolating decision procedure (with support for equality logic, uninterpreted functions, and limited support for bit-vector operations), and
  • an API for third-party decision procedures.
A more detailed description of these features is provided in our CAV tool paper. The architecture and the installation of Wolverine is described in our TACAS competition contribution paper.

Publications

Download

new!

Wolverine 0.5c

Version 0.5c is the (combat-equipped) release of Wolverine which contains a number of adaptations for the first software verification combat... uhm.. competition.

Linux

64-bit


Wolverine 0.5

We provide binaries for Linux, Windows, and OS X, as well as the source code:

Linux

32-bit

64-bit

MacOS X

Universal binary (i386/x86_64/PPC)

Windows

Windows XP/Vista/7 32-bit

Source Code

tarball (July 2011)

The tool DDVerify, which provides a harness and an operating system model annotated with assertions, is available separately.


Older versions:

Linux

64-bit v0.4

64-bit, beta July 2010

Used to produce the results reported in [Weissenbacher, 2010]. Includes a collection of simplified Windows device drivers, and a modified version of the DDVerify source file (replacing the source files in DDVerify's bin-directory in ddverify-2010-04-30.tgz).

MacOS X

Intel x86_64 v0.4

Source Code

Release 01-26-11