Towards certifying domain-specific properties of synthesized code

G. Roşu, J. Whittle

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

4 Citations (Scopus)


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
Number of pages6
ISBN (Electronic)0769517366, 9780769517360
Publication statusPublished - 1 Jan 2002
Externally publishedYes
EventAutomated Software Engineering Conference 2002 - Edinburgh, United Kingdom
Duration: 23 Sept 200227 Sept 2002
Conference number: 17th

Publication series

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


ConferenceAutomated Software Engineering Conference 2002
Abbreviated titleASE 2002
Country/TerritoryUnited Kingdom

Cite this