ICS: Integrated Canonizer and Solver

Jean-Christophe Filliatre, Sam Owre, Harald Ruess, N. Shankar

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


Abstract

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.


Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems