Download

Set of selected interpolants used for benchmarking. 

Interpolants were extracted, as single-output AIG circuits, from model checking runs on publicly available benchmarks from the HWMCC set (http://fmv.jku.at/hwmcc17/). 
They were selected by considering size, SAT time, and circuit sampling, among non trivially solved problems.

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

README

In order to reproduce the experimental results presented in our journal pubblication "Logic Synthesis for Interpolant Circuit Compaction", we present in this txt file a description of PdTRAV and ABC commands used.