ICS (Integrated Canonizer and Solver) is a decision procedure developed at SRI International that efficiently decides formulas in a combination of useful theories. It provides an API that makes it suitable for use in applications with highly dynamic environments such as proof search or symbolic simulation.

ICS decides the satisfiability of formulas in a quantifier-free, first-order theory containing both uninterpreted function symbols and interpreted symbols from a rich combination of datatype theories, including arithmetic, tuples, arrays, and bit-vectors. This theory is particularly interesting for many applications in software and hardware verification.

ICS is capable of deciding the satisfiability/validity of sequences of formulas.

x+2 = y |- f(a[x:=3][y-2]) = f(y-x+1) f(y-1)-1 = y+1 , f(x)+1 = x-1 , x+1 = y |- false f(f(x)-f(y)) <> f(z) , y <= x , y >= x+z , z > 0 |- falseHere

- Equality and disequality.
- Rational and (incomplete) integer linear arithmetic.
- Tuples and projections from tuples.
- Coproducts. Together with tuples, coproducts are used to build up ground datatype terms.
- Boolean constants.
- S-expressions builtup from
`car`,`cdr`, and`cons`. - Functional arrays.
- Combinatory logic with case-splitting.
- Bitvector terms include constants, concatenation, extraction.
- There are also (incomplete) extensions to handle nonlinear multiplication.

ics> assert f(f(x)-f(y)) <> f(z). :ok s1 ics> assert y <= x. :ok s2 ics> assert y >= x + z. :ok s3 ics> assert z > 0. :unsat {-1 * y + x >=0, z >0, -1 * z + y + -1 * x >=0}ICS returns a list of the asserted atoms that participate in demonstrating the inconsistency.

This sequence of assertions can also placed in a file `foo.ics`
and ICS can be invoked in batch mode as a shell command

$ ics foo.ics :unsat {-1 * y + x >=0, z >0, -1 * z + y + -1 * x >=0}

The SAT solver can also be used interactively as

ics> sat [x > 2 | x < 4 | p] & 2 * x > 6. :sat s5 :model [p |-> :true][-6 + 2 * x > 0]

This sat command returns an assignment for the propositional variable
`p` and a subset of the input literals.
Here, satisfying assignments for `x` are described by means of
the constraint `-6 + 2 * x > 0`.

Verification conditions are usually proved within the context of a large number of assertions derived from the antecedents of implications, conditional tests, and predicate subtype constraints. These contexts must be changed in an incremental manner when assertions are either added or removed. Through the use of functional data structures, ICS allows contexts to be incrementally enriched in a side-effect-free manner.

ICS is implemented in Ocaml, which offers satisfactory run-time performance, efficient garbage collection, and interfaces well with other languages such as C. ICS uses arbitrary precision rational numbers from the GNU multi-precision library GMP. There is a well-defined API for manipulating ICS terms, asserting formulas to the current database, switching between databases, and functions for canonizing terms. This API is packaged as

- a C shared-object library,
- an Ocaml object module,
- a CommonLisp foreign-function interface, and
- an interactor

ICS can be used as a back-end decision procedure in a variety of applications like static analysis, abstract interpretation, extended type checking, symbolic simulation, model checking, and compiler optimization.

Forthcoming versions of ICS will extend its range of theories and capabilities; in particular, the next version of ICS will be complete for integer linear arithmetic and will handle a larger subset of nonlinear real arithmetic.

Back to the main ICS homepage