NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
AutoBayes/CC: Combining Program Synthesis with Automatic Code Certification: System DescriptionCode certification is a lightweight approach to formally demonstrate software quality. It concentrates on aspects of software quality that can be defined and formalized via properties, e.g., operator safety or memory safety. Its basic idea is to require code producers to provide formal proofs that their code satisfies these quality properties. The proofs serve as certificates which can be checked independently, by the code consumer or by certification authorities, e.g., the FAA. It is the idea underlying such approaches as proof-carrying code [6]. Code certification can be viewed as a more practical version of traditional Hoare-style program verification. The properties to be verified are fairly simple and regular so that it is often possible to use an automated theorem prover to automatically discharge all emerging proof obligations. Usually, however, the programmer must still splice auxiliary annotations (e.g., loop invariants) into the program to facilitate the proofs. For complex properties or larger programs this quickly becomes the limiting factor for the applicability of current certification approaches.
Document ID
20020090879
Acquisition Source
Ames Research Center
Document Type
Preprint (Draft being sent to journal)
Authors
Whalen, Michael (Minnesota Univ. Minneapolis, MN United States)
Schumann, Johann (NASA Ames Research Center Moffett Field, CA United States)
Fischer, Bernd (NASA Ames Research Center Moffett Field, CA United States)
Clancy, Daniel
Date Acquired
September 7, 2013
Publication Date
January 1, 2002
Subject Category
Computer Programming And Software
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Related Records

There are no records associated with this record.
No Preview Available