Downloads
Overview Search Downloads Up
Category: PdTrav Package
Order by: Default | Name | Date | Hits | [Descending]
Files:
PdTrav (static linux exe submitted at HWMCC2014) Version:3.3.0

(3 votes)

Download
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 (source code) starting from April 2013. The complete kit, named pdtools (current 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

 

 

 




Created
Size
Downloads
2014-06-27 22:36:15
0 B
457
pdtools-1.3.0

(1 vote)

Download
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 (source code) starting from April 2013. The complete kit, named pdtools (current version 1.3.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.




Created
Size
Downloads
2013-04-09 07:36:10
6.42 MB
566