Embedded Deduction With ICS

---

Authors

Leonardo de Moura and Harald Rue{\ss} and John Rushby and Natarajan Shankar

Abstract

Formal analyses can provide valuable assurance for high confidence software and systems. The analyses can range from strong typechecking through test case generation and static analysis to model checking and full verification. In all cases, the tools that support the analyses use formal deduction in some way or other. ICS is a fully automatic, high-performance decision procedure for a broad combination of theories that can be embedded in all tools of this kind to provide them with a core deductive capability of exceptional power and performance. We describe the design choices underlying ICS and the capabilities it provides.

gzipped postscript or postscript

BibTeX Entry

@MISC{deMoura-etal:HCSS03,
	AUTHOR = {Leonardo de Moura and Harald Rue{\ss} and John Rushby and Natarajan Shankar},
	TITLE = {Embedded Deduction With {ICS}},
	HOWPUBLISHED = {Presented at the National Security Agency's
		        Third High Confidence Software and Systems Conference},
	MONTH = apr,
	YEAR = 2003,
        NOTE = {Available at \url{http://www.csl.sri.com/~ruess/papers/HCSS03-2/hcss03.ps}}
}

---

Harald Ruess: ruess@csl.sri.com