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.

• Type: Conference
• Year: 2004
• Where: CADE
• Authors: Bernd Fischer 0002, Ewen Denney, Johann Schumann
• Keywords: Automated Reasoning, CADE 2004, First-order Theorem Prover, Individual Simplification Stages, Proof Obligations