Paper Info
Title
ICS: Integrated Canonizer and Solver
Abstract
Decision procedures are at the core of many industrial-strength verification systems such as ACL2 [KM97], PVS [ORS92], or STeP [MtSg96]. Effective use of decision procedures in these verification systems require the management of large assertional contexts. Many existing decision procedures, however, lack an appropriate API for managing contexts and efficiently switching between contexts, since they are typically used in a fire-and-forget environment. ICS (Integrated Canonizer and Solver) is a decision procedure developed at SRI International. It does not only efficiently decide formulas in a useful combination of theories but it also provides an API that makes it suitable for use in applications with highly dynamic environments such as proof search or symbolic simulation. The theory decided by ICS is a quantifier-free, first-order theory with uninterpreted function symbols and a rich combination of datatype theories including arithmetic, tuples, arrays, sets, and bit-vectors. This theory is particularly interesting for many applications in the realm of software and hardware verification. Combinations of a multitude of datatypes occur naturally in system specifications and the use of uninterpreted function symbols have proven to be essential for many real-world verifications.
Year
DOI
Venue
2001
10.1007/3-540-44585-4_22
Computer Aided Verification
Keywords
Field
DocType
integrated canonizer,first order
Discrete mathematics,Proof search,Computer science,Automated theorem proving,Algorithm,Theoretical computer science,Solver,ACL2,Verification system
Conference
Volume
ISSN
ISBN
2102
0302-9743
3-540-42345-1
Citations 
PageRank 
References 
81
6.44
7
Authors
4
Name
Order
Citations
PageRank
Jean-Christophe Filliâtre161545.86
Sam Owre21323104.39
Harald Rueß352638.69
Natarajan Shankar43050309.55