Sciweavers

CADE
2004
Springer

Using Automated Theorem Provers to Certify Auto-generated Aerospace Software

14 years 5 months ago
Using Automated Theorem Provers to Certify Auto-generated Aerospace Software
Abstract. We describe a system for the automated certification of safety properties of NASA software. The system uses Hoare-style program verification technology to generate proof obligations which are then processed by an automated first-order theorem prover (ATP). For full automation, however, the obligations must be aggressively preprocessed and simplified. We describe the unique requirements this places on the ATP and demonstrate how the individual simplification stages, which are implemented by rewriting, influence the ability of the ATP to solve the proof tasks. Experiments on more than 25,000 tasks were carried out using Vampire, Spass, and e-setheo.
Bernd Fischer 0002, Ewen Denney, Johann Schumann
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2004
Where CADE
Authors Bernd Fischer 0002, Ewen Denney, Johann Schumann
Comments (0)