Overview Search Downloads Up
Download details
(1 vote)

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 ranked within the top 3 model checkers in all HWMCC competitions from 2007 to 2013 (single property ranking, see

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.
A recent description of PdTRAV is available in:

Gianpiero Cabodi, Sergio Nocco, Stefano Quer: "Benchmarking a model checker for algorithmic improvements and tuning for performance".
Formal Methods in System Design 39(2): 205-227 (2011)

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.

A more complete tool description is coming soon.


Size 6.42 MB
Downloads 579
Created 2013-04-09 07:36:10
Created by System
Changed at 2013-04-10 07:31:14
Modified by admin