Download

PdTRAV (Politecnico di Torino Reachability Analysis & Verification)

PdTRAV is an academic tool developed by the Formal Methods Group, as a platform to evaluate Model Checking algorithms. So far it should not be considered as a development/verification tool, but rather as a collection of MC engines.

PdTRAV's most powerful engines are based on Craig interpolation, on BDDs, on IC3.
We also have a multithreaded version of the tool, running several tools on a "winner-takes-it-all" basis. 

Download

PdTRAV (Politecnico di Torino Reachability Analysis & Verification)

PdTRAV is an academic tool developed by the Formal Methods Group, as a platform to evaluate Model Checking algorithms. So far it should not be considered as a development/verification tool, but rather as a collection of MC engines.

PdTRAV's most powerful engines are based on Craig interpolation, on BDDs, on IC3.
We also have a multithreaded version of the tool, running several tools on a "winner-takes-it-all" basis. 

PdTRAV is available starting from April 2013. The complete kit, named pdtools (this version 1.4.0), includes packages from other groups:

abc (A.Mishchenko)
minisat (N.Een, N,Sörensson)
cudd (F.Somenzi)
aiger (A.Biere)

We thank the authors of the above mentioned tools for allowing us to publish them in this suite.

To run the multi-threaded version (HWMCC setup):

pdtrav -strategy thrd .aid

you may wish to add -verbosity 1 (-verbosity 4 very verbose)

This is going to start up to 8 threads

If you want to disable some thread (e.g. BMC), use

-thrdDis  BMC

If you want to just enable some thread (e.g. IGR), use

-thrdEn IGR