Loading...
Please wait, while we are loading the content...
Similar Documents
A program certification assistant based on fully automated theorem provers
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Fischer, Bernd Denney, Ewen |
| Copyright Year | 2005 |
| Description | We describe a certification assistant to support formal safety proofs for programs. It is based on a graphical user interface that hides the low-level details of first-order automated theorem provers while supporting limited interactivity: it allows users to customize and control the proof process on a high level, manages the auxiliary artifacts produced during this process, and provides traceability between the proof obligations and the relevant parts of the program. The certification assistant is part of a larger program synthesis system and is intended to support the deployment of automatically generated code in safety-critical applications. |
| File Size | 18123785 |
| Page Count | 16 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20050184118 |
| Archival Resource Key | ark:/13960/t6vx5b40b |
| Language | English |
| Publisher Date | 2005-01-24 |
| Access Restriction | Open |
| Subject Keyword | Mathematical And Computer Sciences (general) Theorem Proving Graphical User Interface Automatic Control Applications Programs Computers Safety Architecture Computers Certification 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 |