ICS: Integrated Canonizer and Solver


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

	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