dvt: deductive verification tools

[2008-12-03, rev. 2bc020c1c4e8]
Coypright © 2007 Saarland Univerisity

Introduction

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.

Publications

[E07]

Franziska Ebert. Translation Validation for Optimizing Compilers. Master Thesis. 2007

Usage

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.

Documentation

dvt was primarly developed for internal usage in the Verisoft project. It is only sparsely documented. If you have questions please contact Lars Kuhtz.

Obtaining dvt

If you want to try out dvt, please send a request to Lars Kuhtz.

Contact

Lars Kuhtz <kuhtzXcsYuni-sbYde> (substitute X by @ and Y by .)