Skip to content

Latest commit

 

History

History
54 lines (34 loc) · 1.87 KB

README.md

File metadata and controls

54 lines (34 loc) · 1.87 KB
Raw

Dafny Interactive Verification Environment (DIVE)

A new interaction concept for the interactive verification of Dafny programs.

DIVE logo

The logo design is artistically inspired by the Dafny logo.

Build Status

DIVE is developed at the Karlsruhe Institute of Technology.

We develop this interactive program verification environment to promote and experiment with new ways of interaction in program verification. It is a graphical proof front end for programs written and specified in Dafny and supports different types of user guidance for proofs:

  1. Autoactive annotations within the source code can be used to guide the automated prover. (That's how Dafny itself works)
  2. Textual proof scripts can be written to discharge proof obligations in a programmatic fashion.
  3. Interactive point-and-click directives can be used to apply a sequence proof steps to an open proof goal (direct interaction).

DIVE is open source (GPL) and written in Java.

Requirements

  • Java (OpenJDK or Oracle JDK, at least version 11) must be installed.
  • Boogie must be installed and in path (and then, Z3 is also available) For Ubuntu (version 18.04 or higher) run sudo apt-get install boogie. In other cases refer to Boogie Github

Run it

After cloning the repository, invoke ./gradlew run (on Linux/iOS) or gradle.bat run (on Windows).

An example is included in DIVE and accessible in the WelcomePane using the button "Load example".

Boogie

will be called as boogie. Hence it must be in the path.

If not, you can set the path to your boogie executable using an environment variable.