ic3: SAT-Based Model Checking Without Unrolling

Aaron Bradley
MC@CU

Paper

Current version (November 2010): PDF (To appear at VMCAI'11; slides)
Original public version (March 2010): arXiv

Implementation

Version that placed 3rd in HWMCC'10: ic3 v0.1 (statically compiled on 64-bit Ubuntu 9.10).
Note: Using the -v (verbose) option causes ic3 to terminate with one of two exceptions: Safe or CEx.

Somewhat cleaned up (but nevertheless not all that readable) source: ic3.tar.gz

*This research is supported by NSF grant CCF 0952617.