Subproject

S1

Categories

Data structures for symbolic state representation

Overview

Object-oriented AIG (And-Inverter graph) library for representing and manipulating boolean functions. It is especially suited for applications in the field of verification (e.g. for representing state sets in symbolic model-checking). Basis of the LinAIG package.

Publications

F. Pigorsch and C. Scholl. An AIG-based QBF-Solver using SAT for preprocessing. In Sachin S. Sapatnekar, editor, Institute of Electrical and Electronics Engineers (IEEE) Design Automation Conference, pages 170-175, 2010.

F. Pigorsch and C. Scholl. Exploiting structure in an AIG based QBF solver. In Conference on Design, Automation and Test in Europe, pages 1596-1601, 2009.

F. Pigorsch, C. Scholl, and S. Disch. Advanced unbounded CTL model checking by using AIGs, BDD sweeping, and quantifier scheduling. In GI/ITG/GMM Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", pages 135-144, 2006.

F. Pigorsch, C. Scholl, and S. Disch. Advanced unbounded model checking based on AIGs, BDD sweeping, and quantifier scheduling. In Conference on Formal Methods in Computer Aided Design (FMCAD), pages 89-96, 2006.

Benchmarks

---

Download

Click here for library & manual.

Manual

(see above)

Status

Stable