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.

NOTE: we are providing the source code under the MIT license (at It hasn't been built in several years; please let us know if you have any updates, so others can benefit.

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 Ian A. Mason