Skip to content

Latest commit

 

History

History
60 lines (39 loc) · 3.29 KB

README.md

File metadata and controls

60 lines (39 loc) · 3.29 KB
Raw

Voila: Concise Outlines for a Complex Logic

Voila logo

Voila — conference paper at FM'21, an extensive technical report is also available — is a proof outline checker for fine-grained concurrency verification. It supports a simple, Java-like programming language, with specifications based on a concurrent separation logic. Voila uses the Viper verification infrastructure to automatically discharge all proof obligations.

See TicketLock.vl for an example, or browse all examples and regression tests in src/test/resources.

Installation

Prerequisites:

  1. Java: Voila is written in Scala, and runs on the Java Virtual Machine. We recommend Java 11, but newer versions should work as well.

  2. Z3: Voila uses the excellent Z3 SMT solver. We strongly recommend Z3 4.8.7. Add Z3's executable to your path, or let environment variable Z3_EXE point to it.

We provide instructions for Linux, but adapting them for Windows or MacOS should be straightforward.

Pre-built

Download the latest official Voila release, or see all Voila release for alternatives.

Self-built

Install the Scala build tool sbt, version 1.4.4 or newer.

  1. Download this repository into, e.g. ~/voila
  2. Download Silver into ~/voila/silver No longer necessary, since Silicon includes Silver as a Git submodule
  3. Download Silicon into ~/voila/silicon
  4. Create a symlink ~/voila/silver pointing to ~/voila/silicon/silver
  5. Open a terminal, change directory to ~/voila, and start sbt
    1. Compile with sbt command compile
    2. Generate fat jar ~/voila/target/scala-2.13/voila.jar with sbt command assembly
    3. Optional: verify a single file with run, e.g. run src/test/resources/examples/Caper/TicketLock.vl (no verification failures expected)
    4. Optional: run all tests with sbt command test (will take some time)
    5. Quit with sbt command exit

Usage

  1. Open a terminal, change directory to where you downloaded or built Voila, e.g. ~/voila
  2. Run ./voila.sh -i <path_to_file.vl> to verify a file

Demo Session

Recording of a Voila demo session

Authors

Voila is developed at ETH Zurich, by Felix A. Wolf, Malte Schwerhoff, and Peter Müller.

License

Voila is licensed under Mozilla Public License Version 2.0.