Truth Homepage

Truth

Recent Improvements

Truth now supports game based model checking for the alternation free fragment of the mu-calculus

We developed a specification language compiler (SLC) which turns Truth into a generic verification tool for broad range of specification languages

We developed a parallel model checking algorithm for the alternation free fragment of the mu-calculus which is implemented in a dedicated Truth-Version running on a cluster of workstations. A brief description of the algorithm can be found here . Please contact me for further information.

Getting Truth

Truth is available for Solaris and for Linux. To run Truth you need the following software packages:

daVinci A tool for the visualization of graphs

Java(TM) JDK 1.1.1 or higher is freely obtainable, but you need to register.

Java(TM) Swing(TM) Swing Components for JAVA. They are freely obtainable, but you need to register.

Objectspace A Generic Collection Library for Java Version 3.0 or higher is also free if you register.

dotty (graphviz) A tool vor visualization of graphs, similar to davinci. Just used for visualizing game graphs.

Furthermore, the Haskell sources are also available. If you want to compile Truth you need the Glasgow Haskell Compiler. We also provide some locally build ghc packages, usually the latest CVS snapshots which may be more out of date but which are already compiled versions of the compilers.

Click here to get a version of Truth

Information for local developers

Overview of Truth

The latest paper giving an overview of Truth is here. The first version of Truth was implemented by Stephan Tobies during his master thesis as is described in his thesis (in German). A short overview of the system including a small user's guide was then given in this technical report. The system was officially presented in this paper.

The following image gives an overview of the term model checking as it should be unterstood by the tool Truth in future releases.