Towards certifying domain-specific properties of synthesized code

G. Roşu, J. Whittle

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

Abstract

We present a technique for certifying domain-specific properties of code generated using program synthesis technology. Program synthesis is a maturing technology that generates code from high-level specifications in particular domains. For acceptance in safety-critical applications, the generated code must be thoroughly tested which is a costly process. We show how the program synthesis system AUTOFILTER can be extended to generate not only code but also proofs that properties hold in the code. This technique has the potential to reduce the costs of testing generated code.

Original languageEnglish (US)
Title of host publicationProceedings - ASE 2002
Subtitle of host publication17th IEEE International Conference on Automated Software Engineering
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages289-294
Number of pages6
ISBN (Electronic)0769517366, 9780769517360
DOIs
StatePublished - Jan 1 2002
Externally publishedYes
Event17th IEEE International Conference on Automated Software Engineering, ASE 2002 - Edinburgh, United Kingdom
Duration: Sep 23 2002Sep 27 2002

Publication series

NameProceedings - ASE 2002: 17th IEEE International Conference on Automated Software Engineering

Other

Other17th IEEE International Conference on Automated Software Engineering, ASE 2002
Country/TerritoryUnited Kingdom
CityEdinburgh
Period9/23/029/27/02

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Towards certifying domain-specific properties of synthesized code'. Together they form a unique fingerprint.

Cite this