ICS (Integrated Canonizer and Solver) is a
decision procedure developed at SRI International.
It is based on well-developed theory,
it efficiently decides formulas in a useful combination
of theories, and it provides an API that makes
it suitable for use in applications with highly dynamic
environments such as proof search or symbolic simulation.
The efficiency and scalability of ICS in processing formulas,
the richness of its API, and its ability for fast context-switching
make it suitable to use it as a black box for discharging
verification conditions not only in a theorem proving context
but also in a multitude of applications like static analysis,
abstract interpretation, extended type checking,
symbolic simulation, model checking, or compiler optimization.
