Horn-ICE Verification Toolkit
This documents describes how to build and use the Horn-ICE verification toolkit described in the paper "Horn-ICE Learning for Synthesizing Invariants and Contracts".
This toolkit consists of two different verifiers, both using the Horn-ICE Decision Tree Learning Algorithm:
- A verifier built on top of Microsoft Boogie, which verifies programs given in the Boogie verification language
- A verifier for Constrained Horn Clauses built on top of Microsoft Z3, which verifies constrained Horn clauses in the SMTLib2 datalog format (e.g., as produced by SeaHorn)
The following instructions assume a recent Linux operating system (e.g., Ubuntu 16.04). If you are running another operating system, such as Windows or MacOS, we recommend using a virtual machine with Ubuntu 16.04 guest operating system.
The Horn-ICE verification toolkit is portable and can be compiled on MacOS and Windows (e.g., using mingw and MSYS). However, the instructions in this document need to be modified accordingly.
The Horn-ICE verification toolkit requires the following software installed:
- GNU make
- GNU compiler collection (specifically
g++version 5.4 or newer, including support for OpenMP)
- Mono (version 4.2.1 or newer)
- Python (2.7 or newer)
Use the following commands to install the required software in Ubuntu 16.04 (or consult the documentation of your Linux distribution):
sudo apt-get install build-essential
sudo apt-get install mono-complete
sudo apt-get install python
Building the Toolkit
The build process is automated. To build the Horn-ICE verification toolkit, simply execute the command
in the folder you have extracted the archive to. This will build the following three components (in this order):
- The Horn-ICE decision tree learning algorithm
- The verifier for constrained Horn clauses (which requires Z3 to be built first)
After building has completed, the compiled binaries of the Boogie-based verifier are located in
./Boogie/Binaries/, while the binaries of the verifier for constraint Horn clauses are located in
You can test whether the build process was successful by following the instructions in the section Running a Single Benchmark.
If you seek to modify any of the components, the remainder of this section explains how to build each in detail. You can also refer to the
Makefile for more information.
To compile Boogie, change into
./Boogie/Source/ and execute the command
xbuild /p:TargetFrameworkVersion="v4.5" /p:TargetFrameworkProfile="" /p:WarningLevel=1 Boogie.sln
The additional options
/p:TargetFrameworkProfile="" are not necessary in general, but are sometimes required in order to fix a specific problem with Mono on Ubuntu 16.04. Warning messages produced during compilation are safe to ignore. The option
/p:WarningLevel=1 sets the warning level to a value that suppresses trivial warnings.
After a successful compilation, the binaries are located in
Z3 4.7.1 is shipped with this toolkit and is located in the folder
./z3-4.7.1/. To build Z3, please follow the instructions in
README.md or on the Z3 website.
Once Z3 has successfully been compiled, copy the file
z3 in the folder
./Boogie/Binaries/ and rename it to
z3.exe. Alternatively, you can specify the file name and location of the Z3 binary using the option
-z3exe: when running Boogie.
The verifier for constrained Horn clauses requires a static library of Z3 to link against. In order to create such a library, change into the directory
./z3-4.7.1/build/ and execute the following command
find . -name '*.o' | xargs ar rs ./z3.a
This creates a file named
Building the Horn-ICE Decision Tree Learning Algorithm
To compile the Horn-ICE Decision Tree Learning Algorithm, change into the directory
./hice-dt/src/ and execute the command
After successful compilation, the binaries are located inside
./hice-dt/src/. Copy the file
hice-dt.exeon Windows) to
Building the Verifier for Constrained Horn Clauses
To compile the Verifier for Constrained Horn Clauses, change into the directory
./chc_verifier/src/ and execute the command
After successful compilation, the binary is located inside
Running a Single Benchmark
The following instructions show how to run a single benchmark using the Boogie-based verifier and the verifier for constrained Horn clauses.
Note: Benchmarks can be found in
The Boogie-Based Verifier
All binaries of the Boogie-based verifier should be present in
Note: It is easiest to run Boogie from inside the
To verify a Boogie
.bpl program, execute the following command inside the
mono Boogie.exe -trace -nologo -noinfer -contractInfer -mlHoudini:./hice-dt -learnerOptions:"-b -h" my_benchmark.bpl
The given options have the following effect:
-trace(optional): prints intermediate results and status information
-nologo(optional): suppresses the printing of the Boogie version at start-up
-noinfer(required): disables some of Boogie's internal static analysis techniques, which interfere with our invariant synthesis approach
-contractInfer(required): enables automatic invariant synthesis
argspecifies the binary of the Horn-ICE learning algorithm (
./hice-dtin our case since we are executing Boogie from the same directory the file
hice-dtis located in)
optionsspecifies options that get passed through to the Horn-ICE learning algorithm as if it were called from the command line (in our case, we run a bounded version
-band use a Houdini pre-phase
-h); multiple options need to be enclosed by quotes
Our extension of Boogie supports most of Boogie's command line options. Please refer to the manual for more information.
Note: The way options are specified differs between Windows and Linux. Use
"-" on Linux and
"/" on Windows.
Note: On Windows, the Horn-ICE Decision Tree Learning Algorithm might have the file extension
.exe. To account for this, use the full file name
hice-dt.exe when giving the option
Note: If you do not want to run Boogie from inside
./Boogie/Binaries/, the option
-mlHoudini: needs to point to the location of the binary of the Horn-ICE learning algorithm. It is best to specify an absolute path.
Note: Boogie generates many temporary files to communicate with the Horn-ICE learning algorithm. These file are safe to remove after a successful verification. Should you be interested in reading these files, the header
./hice-dt/include/boogie_io.h contains descriptions of their format.
Verifier for Constrained Horn Clauses
All binaries of the verifier for constrained Horn clauses should be present in
To verify a constrained Horn clause, execute the following command inside the
Like the Horn-ICE Decision Tree Learning Algorithm, the Verifier for Constrained Horn Clauses takes two options, which are optional and can be used in any combination:
-b: runs the bounded version of the decision tree learner
-h: runs the Houdini pre-phase
Note: The verifier for constrained Horn clauses does not have special library dependencies and can be moved to any other location if desired.
Running the Benchmark Suits
The following instructions describe how the benchmarks can be run on a machine that has the Horn-ICE verification toolkit installed as described above. We provide three different types of benchmarks:
- recursive programs,
- concurrent programs, and
- sequential programs.
The benchmarks are located in the
Running the Entire Benchmark Suite
The entire benchmark suite can be executed using the following command from inside the
Note: Running the entire benchmark suite takes around 7 hours on an Intel Core i3-6006U CPU @ 2 GHz.
runAll.sh script will generate three log files, as described below. The first two files result from the Boogie-based verifier, while the third file from the verifier for Constrained Horn Clauses.
tabulated_recursiveProgramResult.csvlists all the recursive benchmark programs along with the execution details. The execution details includes number of rounds between teacher and learner, number of Positive, Negative and Horn samples, the time taken by the learner and the verification process. Table-1 in the paper contains these details. We have compared the Boogie-based verifier with Ultimate Automizer in Figure 5 using the data from the above mentioned file.
tabulated_concurrentProgramResult.csvlists all the concurrent benchmark programs along with the execution details. The execution details includes number of rounds between teacher and learner, number of Positive, Negative and Horn samples, the time taken by the learner and the verification process. Table 2 in the paper contains these details.
tabulated_sequentialProgramResult.csvlists all the sequential benchmark programs along with the execution time. Table 3 in the Paper contain these details. We have compared the verifier for Constrained Horn Clauses with PDR in Figure 6 using the data from the above mentioned file.
Running an Individual Benchmark Set
./scripts/ directory contains scripts to execute individual sets of benchmarks and to tabulate their results:
The recursive programs can be verified and their results tabulated using the command
sh run_recursivePrograms.sh; sh tabulate_time_recursivePrograms.sh
The concurrent programs can be verified and their results tabulated using the command
sh run_concurrentPrograms.sh; sh tabulate_time_concurrentPrograms.sh
The sequential programs can be verified and their results tabulated using the command
sh run_sequentialPrograms.sh; sh tabulate_time_sequentialPrograms.sh
Comparing Horn-ICE to Other Tools
The remainder of this document explains how we compared Horn-ICE to other tools.
Experimental Results Mentioned in the Paper
The experimental results described in the paper "Horn-ICE Learning for Synthesizing Invariants and Contracts" can be reproduced as follows:
Table 1 to 3 can be produced using the following command inside the
Figure 5 and 6 have been constructed using the above data along with the experimental results obtained by running the verification tools Ultimate Automizer and PDR on the same environment. For more details, see the information below.
Verification using Ultimate Automizer
Download Ultimate Automizer form https://github.com/ultimate-pa/ultimate/releases.
If you want to build Ultimate Automizer yourself, follow the instructions in the file
README. Otherwise, you can use a pre-compiled package.
Running the Entire Recursive Programs using Ultimate Automizer
The entire recursive program benchmarks can be verified using the following command inside the
sh run_recursivePrograms_Ultimate.sh path_to_Ultimate.py; sh tabulate_time_recursivePrograms_Ultimate.sh
Note: The script
run_recursivePrograms_Ultimate.sh takes one mandatory argument, the path to
Ultimate.py (where the Ultimate Automizer binaries are located).
Note: Z3 needs to be accessible from inside
./scripts/ (e.g., copy it there).
The above command will produce a file named
tabulated_recursiveProgramResult_Ultimate.csv, which lists all recursive benchmarks together with the time taken to verify them.
Verification of Constrained Horn Clauses (Sequential Program) using PDR
The default CHC verification engine of
Z3 4.7.1 is PDR. The following command inside the
./z3-4.7.1/build/ directory can be used to verify the Constrained Horn Clauses using PDR:
Running the Entire Sequential Benchmark Set using PDR
The entire set of sequential programs (in form of Constrained Horn Clauses) can be verified using the following command inside the
sh run_sequentialPrograms_PDR.sh; sh tabulate_time_sequentialPrograms_PDR.sh
Note: Z3 needs to be accessible from inside
./scripts/ (e.g., copy it there).
The above command produces a file named
tabulated_sequentialProgramResult_PDR.csv, which lists all the sequential benchmarks together with the time taken to verify them.