Forgot your password?
New user?
SAL decision procedures
Mathematical Procedures for Decision Problems
Simplify Prover Benchmarks
Yices
Document Actions
ICS
Decision procedure
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.