Towards certifying domain-specific properties of synthesized code

G. Roşu, J. Whittle

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

6 Citations (Scopus)

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
Title of host publicationProceedings - ASE 2002
Subtitle of host publication17th IEEE International Conference on Automated Software Engineering
PublisherIEEE, Institute of Electrical and Electronics Engineers
Pages289-294
Number of pages6
ISBN (Electronic)0769517366, 9780769517360
DOIs
Publication statusPublished - 1 Jan 2002
Externally publishedYes
EventAutomated Software Engineering Conference 2002 - Edinburgh, United Kingdom
Duration: 23 Sep 200227 Sep 2002
Conference number: 17th

Publication series

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

Conference

ConferenceAutomated Software Engineering Conference 2002
Abbreviated titleASE 2002
CountryUnited Kingdom
CityEdinburgh
Period23/09/0227/09/02

Cite this