VeriCool 3

VeriCool 3 is an automatic program verifier for Java-like programs.

Documentation

Symbolic Execution for Implicit Dynamic Frames. [pdf][soundness proof]
Jan Smans, Bart Jacobs, Frank Piessens. Draft.
Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic. [pdf]
Jan Smans, Bart Jacobs, Frank Piessens. ECOOP, 2009.

Downloads

The following releases are currently available for download:

VeriCool requires Windows XP/Vista/7 and Java 1.5 or higher. VeriCool includes the Z3 theorem prover.

last update: februari 28 2012