ICS: Integrated Canonizer and Solver

---

Authors

Jean-Christophe Filliatre and Sam Owre and Harald Rueß and N. Shankar

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.

gzipped postscript or postscript

BibTeX Entry

@unpublished{FilliatreOwreRuessShankar:CAV2001,
  TITLE = {ICS: Integrated Canonizer and Solver},
  AUTHOR = {Jean-Christophe Filli{\^a}tre and Sam Owre and Harald Rue{\ss} and N. Shankar},
  YEAR = 2001,
  NOTE = {To be presented at CAV'2001}
}

---

Harald Ruess: ruess@csl.sri.com