IIMC

IIMC

Description: IImc is a model checker for AIGER 1.9 models. The name stands for Incremental, Inductive model checker. It checks invariants, language emptiness, and CTL properties. It is written in C++11. IImc's philosophy is Incremental, Inductive Verification (IIV). It is built around three IIV engines: IC3 for safety properties, Fair for omega-regular properties, and IICTL for CTL with fairness. IImc has a few other engines, both BMC-based and BDD-based for both safety and progress properties. It uses CUDD, zchaff, and minisat. Version 1.2 is available from http://iimc.colorado.edu

VO Integration: No

Active: Yes

Available Benchmarks: No

Website: http://ecee.colorado.edu/~bradleya/iimc/

Download: Contact authors.

Documentation: There are relevant publications on the main webpage.

Contact: See list of contributors on main webpage.

Excerpt from: https://www.src.org/library/publication/p068815/