Actions for A Program Certification Assistant Based on Fully Automated Theorem Provers

Email RIS file
Bookmark
Report an Issue

A Program Certification Assistant Based on Fully Automated Theorem Provers

Author
Denney, Ewen
Published
January 24, 2005.
Physical Description
1 electronic document
Additional Creators
Fischer, Bernd
Online Version

Availability

I Want It
I Want It

Finding items...

Restrictions on Access
Unclassified, Unlimited, Publicly available.
Free-to-read Unrestricted online access
Summary
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.
Other Subject(s)
Collection
NASA Technical Reports Server (NTRS) Collection.
Note
Document ID: 20050184118.
User Interfaces for Theorem Provers (UITP 2005); 9 Apr. 2005; Edinburgh, Scotland; United Kingdom.
Terms of Use and Reproduction
Copyright, Distribution under U.S. Government purpose rights.
View MARC record | catkey: 15963266