Tools

Throughout the course, we will use the Viper verification infrastructure and the SMT solver Z3. Installation instructions are found below. Please bring a device on which these tools are installed to each lecture.

Viper

The Viper verification infrastructure comprises a programming language (silver but also often just called Viper) and two verification backends (called silicon and carbon).

To install Viper, first make sure that a 64-bit version (e.g. OpenJDK) of Java 11+ is installed on your machine. This may not be the default installation on your machine (for example when installing through a package manager) or the default version offered as a download. Furthermore, make sure that the JAVA_HOME environment variable points to your Java installation (details).

We will use Viper through the Viper IDE, an extension to the free, open-source editor Microsoft Visual Studio Code (VS Code for short).

To install the Viper IDE proceed as follows:

  1. Make sure to have the latest version of VS Code (64-bit) installed.
  2. Open VS Code
  3. Go to the extension browser (⇧+Ctrl+X or ⇧+⌘+X)
  4. Search for Viper (see screenshot below).
  5. Install the extension and restart VS Code.
  6. Create an empty file test.vpr and open it with VS Code.
  7. The Viper extension should now install all required dependencies.
  8. If everything works, the Viper IDE should report verification successful for the file test.vpr.

Viper IDE extension

Z3

We will also use the SMT solver Z3, originally developed by Microsoft research.

Precompiled binaries for most operating systems are available here.

Alternatively, you can use the python tool pysmt to install Z3, use the docker image, or compile Z3 yourself.

To test your installation of Z3, run the command line tool create a file test.smt2 with the following content:

(declare-const p Bool)
(assert (and p (not p))) 
(check-sat)

Running z3 test.smt2 should then output unsat.