T2 Temporal Prover
The T2 research project aims to build a high-performance automatic program verification tool for proving temporal properties of programs, such as safety, termination, or properties specified in the logic CTL. T2 replaces the original TERMINATOR project, which was started in 2005. See the authors named in the list of publications for an idea of who has contributed to T2 and TERMINATOR over the years.
To build T2, we recommend using Visual Studio (2013 or later), but you can also follow the Mono instructions provided below. In VS, the F# Power Pack is managed through NuGet in Visual Studio and does not need to be downloaded manually.
To build T2, you first need to build the .NET bindings of z3 using Mono. For this, get the z3 sources (4.3.2 is known to work) from http://z3.codeplex.com/
To install needed .NET libraries, you will need NuGet, which you can obtain from http://nuget.org/nuget.exe.
Let $NUGET be the path to your nuget.exe download, $Z3DIR be the directory
with Z3 sources, $T2DIR be the T2 source directory (e.g., set them by
export Z3DIR=/path/to/z3/) and follow these steps:
Install software needed for the build process:
g++pythonxbuildfsharpOn a Debian (>> squeezy) or Ubuntu (>= 14.04 LTS) system, this suffices:
$ sudo apt-get install build-essential python mono-complete mono-xbuild fsharp
On OS X, install the Mono MDK for Mac OS from
http://www.mono-project.com/download/
and install the XCode development tools (e.g., by executing gcc in
a Terminal -- if it's not there yet, Mac OS will offer to install XCode).
Build z3. On Linux, this suffices:
$ pushd "$Z3DIR"
$ ./configure
$ pushd "$Z3DIR/build"
$ make
$ popd && popd
On OS X, you need to enforce a 32bit build (for compatibility with Mono):
$ pushd "$Z3DIR"
$ ./configure
$ pushd "$Z3DIR/build"
$ perl -i -pe 's/-D_AMD64_/-arch i386/; s/LINK_EXTRA_FLAGS=/$&-arch i386 /' config.mk
$ make
$ popd && popd
Build the .NET bindings for z3:
$ pushd "$Z3DIR/src/api/dotnet/"
$ echo -e '<configuration>\n <dllmap dll="libz3.dll" target="libz3.dylib" os="osx"/>\n <dllmap dll="libz3.so" target="libz3.dylib" os="linux"/>\n</configuration>\n' > Microsoft.Z3.config
$ xbuild Microsoft.Z3.csproj
$ popd
Update z3 and its .NET bindings in the T2 source tree:
$ cp "$Z3DIR/src/api/dotnet/obj/Debug/Microsoft.Z3.*" "$T2DIR/src/"
$ cp "$Z3DIR/build/libz3.*" "$T2DIR/src/"
Get required packages via NuGet (may need to import certificates first):
$ mozroots --import --sync
$ pushd "$T2DIR/src" && mono $NUGET restore && popd
Build T2, in Debug mode:
$ pushd "$T2DIR/src" && xbuild && popd
In Release configuration:
$ pushd "$T2DIR/src" && xbuild /property:Configuration=Release && popd
Run T2 as follows (replace Debug by Release for the release build)
$ mono "$T2DIR/src/bin/Debug/T2.exe"
For example, to execute the testsuite:
$ pushd "$T2DIR/test" && mono "$T2DIR/src/bin/Debug/T2.exe" -tests
T2 is run from the command line, and the following command line arguments are used to define the proof goal:
-input_t2 string:
Path of the input file in T2 syntax. For examples, look at test/*.t2.
-termination:
Try to prove (non)termination.
-safety int:
Try to prove non-reachability of location int.
-ctl CTL_Formula:
Try to prove that CTL_Formula holds for the program.
The formula format is as follows:
[AG], [EF], and [AW].[AG](x > 0) and [EF]([AG](y < x)).
For more CTL formula examples, see programTests.fs, or the parser
definition in absparse.mly.-fairness Fairness_Condition:
Try to prove termination/a CTL formula under Fairness_Condition.
The format of Fairness_Condition is (P, Q), where a
computation is unfair if an infinite number of states in it
satisfy P, whereas Q is only satisfied finitely often.
An example is (P == 1, Q == 1), and more examples can be
found in programTests.fs.
Commonly used options that modify T2 output behaviour:
-timeout int
Set timeout (in seconds).
-print_proof:
Print an explanation of the result.
-log:
Turn on verbose logging. This will print a lot of output, and may
be hard to understand for non-developers.
Typical calls of T2 on Windows, with output, look like this:
$ src/bin/Debug/T2.exe -input_t2 test/testsuite/small02.t2 -safety 10000 -timeout 42
Safety proof succeeded
$ src/bin/Debug/T2.exe -input_t2 test/testsuite/small01.t2 -termination -print_proof
Termination proof succeeded
Used the following cutpoint-specific lexicographic rank functions:
* For cutpoint 7, used the following rank functions/bounds (in descending priority order):
- RF x, bound 2
$ src/bin/Debug/T2.exe -input_t2 test/testsuite/heidy1.t2 -CTL "[AG] (x_1 >= y_1)"
Temporal proof succeeded
$ src/bin/Debug/T2.exe -input_t2 test/bakery.t2 -CTL "[AG](NONCRITICAL <= 0 || ([AF](CRITICAL > 0)))" -fairness "(P == 1, Q == 1)"
Temporal proof succeeded
Note that T2 creates "defect" files when proofs fail and logging is enabled. A defect.tt file can be viewed with sdvdefect.exe (which comes with the SDV distribution).