Loading...
Please wait, while we are loading the content...
Similar Documents
Using automated theorem provers to certify auto-generated aerospace software
| 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). 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. |
| File Size | 880216 |
| Page Count | 13 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20040068177 |
| Archival Resource Key | ark:/13960/t5n926q2s |
| Language | English |
| Publisher Date | 2004-01-01 |
| Access Restriction | Open |
| Subject Keyword | Cybernetics, Artificial Intelligence And Robotics Theorem Proving Safety Factors Automatic Control Computer Systems Programs Program Verification Computers Aerospace Engineering Arithmetic Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Article |
