Wolverine

Wolverine: battling bugs with interpolants. Wolverine is a software verifier that checks safety properties of sequential ANSI-C and C++ programs, deploying Craig interpolation to derive program invariants. We describe the underlying approach and the architecture, and provide instructions for installation and usage.