Certification support for automatically generated programs

J. Schumann, B. Fischer, M. Whalen, J. Whittle

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Scopus citations

Abstract

Although autocoding techniques promise large gains in software development productivity, their "real-world" application has been limited, particularly in safety-critical domains. Often, the major impediment is the missing trustworthiness of these systems: demonstrating - let alone formally certifying - the trustworthiness of automatic code generators is extremely difficult due to their complexity and size. We develop an alternative product-oriented certification approach which is based on five principles: (1) trustworthiness of the generator is reduced to the safety of each individual generated program; (2) program safety is defined as adherence to an explicitly formulated safety policy; (3) the safety policy is formalized by a collection of logical program properties; (4) Hoare-style program verification is used to show that each generated program satisfies the required properties; (5) the code generator itself is extended to automatically produce the code annotations required for verification. The approach is feasible because the code generator has full knowledge about the program under construction and about the properties to be verified. It can thus generate all auxiliary code annotations a theorem prover needs to discharge all emerging verification obligations fully automatically. Here we report how this approach is used in a certification extension for AutoBayes, an automatic program synthesis system which generates data analysis programs (e.g., for clustering and time-series analysis) from declarative specifications. In particular, we describe how a variable-initialization-before-use safety policy can be encoded and certified.

Original languageEnglish (US)
Title of host publicationProceedings of the 36th Annual Hawaii International Conference on System Sciences, HICSS 2003
EditorsRalph H. Sprague
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)0769518745, 9780769518749
DOIs
StatePublished - Jan 1 2003
Event36th Annual Hawaii International Conference on System Sciences, HICSS 2003 - Big Island, United States
Duration: Jan 6 2003Jan 9 2003

Publication series

NameProceedings of the 36th Annual Hawaii International Conference on System Sciences, HICSS 2003

Conference

Conference36th Annual Hawaii International Conference on System Sciences, HICSS 2003
Country/TerritoryUnited States
CityBig Island
Period1/6/031/9/03

Fingerprint

Dive into the research topics of 'Certification support for automatically generated programs'. Together they form a unique fingerprint.

Cite this