---

ICS: Integrated Canonizer and Solver

• Jean-Christophe Filliâtre, Sam Owre, Harald Rueß, and N. Shankar
• Computer-Aided Verification, CAV '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.

gzipped postscript or postscript

BibTeX Entry

@inproceedings{ICS:CAV01,
	AUTHOR = {J.-C. Filli{\^a}tre and S. Owre and H. Rue{\ss} and N. Shankar},
	TITLE = {{ICS: Integrated Canonization and Solving}},
        BOOKTITLE = {Computer-Aided Verification, CAV '2001}
	EDITOR = {G. Berry and H. Comon and A. Finkel},
	PAGES = {246--249},
        MONTH = jul,
        YEAR = 2001,
        PUBLISHER = {Springer-Verlag},
        ADDRESS = {Paris, France},
        SERIES = {Lecture Notes in Computer Science},
	VOLUME = 2102
}

---

Sam Owre: owre@csl.sri.com