@inproceedings{8691488852834ffc8eb81fb81831804a,
title = "Towards certifying domain-specific properties of synthesized code",
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.",
author = "G. Ro{\c s}u and J. Whittle",
year = "2002",
doi = "10.1109/ASE.2002.1115032",
language = "English (US)",
series = "Proceedings - ASE 2002: 17th IEEE International Conference on Automated Software Engineering",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "289--294",
booktitle = "Proceedings - ASE 2002",
address = "United States",
note = "17th IEEE International Conference on Automated Software Engineering, ASE 2002 ; Conference date: 23-09-2002 Through 27-09-2002",
}