Integrated Canonizer and Solver


ICS is deprecated and no longer supported (since August 2006)

Please use Yices instead; Yices is much faster, handles more theories, and has several other advantages.


ICS (Integrated Canonizer and Solver) is an efficient decision procedure for a fragment of first-order logic. Terms are built from uninterpreted function symbols and operators from a rich combination of datatypes including arithmetic, functional arrays, tuples, cotuples, and fixed-sized bitvectors. It incorporates a state-of-the-art SAT solver.

ICS can be used as a standalone application that reads formulas interactively, and may also be included as a library in any application that requires embedded deduction.

ICS is one of the SRI FormalWare tools.


Last modified: Fri Aug 25 2006 by John Rushby