- Daniel Kröning
- Georg Weissenbacher
- Google groups:
Interpolation-based Model Checking
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
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.
Publications
- Wolverine: Battling Bugs with Interpolants (competition contribution)
- Program Analysis with Interpolants
- Interpolation-based Software Verification with Wolverine
- Program Analysis with Interpolants
- An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
- Lifting Propositional Interpolants to the Word-Level
- Interpolant Strength
Download
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 |
---|
Wolverine 0.5
We provide binaries for Linux, Windows, and OS X, as well as the source code:
Linux | ||
---|---|---|
MacOS X | ||
Windows | ||
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:
- The experiments in our CAV tool paper are based on version 0.4.
Linux | ||
---|---|---|
Used to produce the
results reported in
[Weissenbacher,
2010]. Includes a collection of simplified
Windows device drivers, and a modified version of
the |
||
MacOS X | ||
Source Code |