Loading...
Please wait, while we are loading the content...
Similar Documents
An empirical evaluation of automated theorem provers in software certification
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Schumann, Johann Fischer, Bernd Denney, Ewen |
| Copyright Year | 2004 |
| Description | 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). We discuss the unique requirements this application places on the ATPs, focusing on automation, proof checking, and usability. For full automation, however, the obligations must be aggressively preprocessed and simplified, and we demonstrate how the individual simplification stages, which are implemented by rewriting, influence the ability of the ATPs to solve the proof tasks. Our results are based on 13 certification experiments that lead to more than 25,000 proof tasks which have each been attempted by Vampire, Spass, e-setheo, and Otter. The proofs found by Otter have been proof-checked by IVY. |
| File Size | 1557383 |
| Page Count | 20 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20040084375 |
| Archival Resource Key | ark:/13960/t3sv2jh4d |
| Language | English |
| Publisher Date | 2004-01-01 |
| Access Restriction | Open |
| Subject Keyword | Computer Programming And Software Theorems Simplification Systems Engineering Safety Factors Proving Mathematical Models Program Verification Computers Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Article |
