T2

T2 Temporal Prover

This project is maintained by mmjb and hkhlaaf.

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.

Building T2

Windows

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.

Using Mono (for Linux and MacOS)

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:

  1. Install software needed for the build process:

    • g++
    • python
    • Mono for .NET 4.0
    • xbuild
    • fsharp

    On 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).

  2. 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
    
  3. 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
    
  4. 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/"
    
  5. Get required packages via NuGet (may need to import certificates first):

      $ mozroots --import --sync
      $ pushd "$T2DIR/src" && mono $NUGET restore && popd
    
  6. Build T2, in Debug mode:

      $ pushd "$T2DIR/src" && xbuild && popd
    

    In Release configuration:

      $ pushd "$T2DIR/src" && xbuild /property:Configuration=Release && popd
    
  7. 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
    

Running T2

T2 is run from the command line, and the following command line arguments are used to define the proof goal:

Commonly used options that modify T2 output behaviour:

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).

Publications

Press