Embedded Deduction With ICS

In: NSA's Third High Confidence Software and Systems Conference.
Authors
Leonardo de Moura, Harald Rueß, 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.
Download: PS, PDF
BibTeX Entry 
@inproceedings{dMRRS:HCSS03,
  TITLE = {Embedded Deduction With ICS},
  AUTHOR = {Leonardo de Moura and Harald Rue{\ss} and John Rushby and Natarajan Shankar},
  BOOKTITLE = {HCSS'03---High Confidence Software and Systems Conference},
  EDITOR = {Brad Martin},
  MONTH = {1-3 April},
  YEAR = {2003},
  ADDRESS = {Baltimore, MD}
}
Leonardo de Moura: demoura@csl.sri.com