Embedded Deduction With ICS

Leonardo de Moura, Harald Ruess, John Rushby, and Natarajan Shankar

Presented at the National Security Agency's Third High Confidence Software and Systems Conference, Baltimore MD, April 2003

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 plain postscript or PDF

Slides

gzipped postscript, or plain postscript or pdf or crude ascii (for your Palm Pilot)

BibTeX Entry

@MISC{deMoura-etal:HCSS03,
	AUTHOR = {Leonardo de Moura and Harald Ruess 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/~rushby/abstracts/hcss03}}
}
Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page