AutoBayes/CC – Combining Program Synthesis with Automatic Code Certification
Loading...
View/Download File
Persistent link to this item
Statistics
View StatisticsJournal 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.