Between Dec 19, 2024 and Jan 2, 2025, datasets can be submitted to DRUM but will not be processed until after the break. Staff will not be available to answer email during this period, and will not be able to provide DOIs until after Jan 2. If you are in need of a DOI during this period, consider Dryad or OpenICPSR. Submission responses to the UDC may also be delayed during this time.
 

AutoBayes/CC – Combining Program Synthesis with Automatic Code Certification

Loading...
Thumbnail Image

View/Download File

Persistent link to this item

Statistics
View Statistics

Journal Title

Journal ISSN

Volume Title

Title

AutoBayes/CC – Combining Program Synthesis with Automatic Code Certification

Published Date

2002

Publisher

Springer-Verlag

Type

Report

Abstract

Code certication is a lightweight approach to formally demonstrate software quality. It concentrates on aspects of software quality that can be dened 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 satises these quality properties. The proofs serve as certicates which can be checked independently, by the code consumer or by certication authorities, e.g., the FAA. It is the idea underlying such approaches as proof-carrying code. Code certication can be viewed as a more practical version of traditional Hoare-style program verication. The properties to be veried 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 certication approaches. Our work combines code certication with automatic program synthesis which makes it possible to automatically generate both the code and all necessary annotations for fully automatic certication. By generating detailed annotations, one of the biggest obstacles for code certication is removed and it becomes possible to automatically check that synthesized programs obey the desired safety properties.

Keywords

Description

Associated research group: Critical Systems Research Group

Related to

Replaces

License

Series/Report Number

Funding information

Isbn identifier

Doi identifier

Previously Published Citation

Proceedings of Conference on Automated Deduction (CADE) 18

Other identifiers

Suggested citation

Whalen, Michael; Fischer, Bernd; Schumann, Johann. (2002). AutoBayes/CC – Combining Program Synthesis with Automatic Code Certification. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/217339.

Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.