dvt: deductive verification tools
[2008-12-03, rev. 2bc020c1c4e8]
Coypright © 2007 Saarland Univerisity
dvt implements a deductive approach for proving refinement relations between reactive systems. Each system may consist of different processes represented as (infinite state) labeled transition systems that communicate through shared memory. The concept is based on a variant of generalized verification diagrams introduced by Manna and Pnueli. dvt includes facilities that support development and debugging of verification diagrams. Proof conditions are discharged using various SMT solvers (simultaneously). The verification of LTL properties is supported through an interface to the SPIN model checker. Beside classical simulation relations dvt can be used to establish refinement relations that preserver liveness properties.
There is an extension that does automatic translation validation for the C0 compiler of the Verisoft project.
|[E07]||Franziska Ebert. Translation Validation for Optimizing Compilers. Master Thesis. 2007|
Please, take a look into the tools folder. In order to get comprehensive information on the usage of a particular program call that program with the option “—help”. Examples can be found in the test folder.
If you want to try out dvt, please send a request to Lars Kuhtz.
Lars Kuhtz <kuhtzXcsYuni-sbYde> (substitute X by @ and Y by .)