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.