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.
Prerequisites:
-
Java: Voila is written in Scala, and runs on the Java Virtual Machine. We recommend Java 11, but newer versions should work as well.
-
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_EXEpoint to it.
We provide instructions for Linux, but adapting them for Windows or MacOS should be straightforward.
Download the latest official Voila release, or see all Voila release for alternatives.
Install the Scala build tool sbt, version 1.4.4 or newer.
- Download this repository into, e.g.
~/voila Download Silver intoNo longer necessary, since Silicon includes Silver as a Git submodule~/voila/silver- Download Silicon into
~/voila/silicon - Create a symlink
~/voila/silverpointing to~/voila/silicon/silver - Open a terminal, change directory to
~/voila, and startsbt- Compile with sbt command
compile - Generate fat jar
~/voila/target/scala-2.13/voila.jarwith sbt commandassembly - Optional: verify a single file with
run, e.g.run src/test/resources/examples/Caper/TicketLock.vl(no verification failures expected) - Optional: run all tests with sbt command
test(will take some time) - Quit with sbt command
exit
- Compile with sbt command
- Open a terminal, change directory to where you downloaded or built Voila, e.g.
~/voila - Run
./voila.sh -i <path_to_file.vl>to verify a file
Voila is developed at ETH Zurich, by Felix A. Wolf, Malte Schwerhoff, and Peter Müller.
Voila is licensed under Mozilla Public License Version 2.0.