Towards Certifying Domain-Specific Properties of Synthesized Code - Extended Abstract -
Grigore Roşu, Jon Whittle · 2002
Grigore Rosu NASA Ames Research Center - USRA/RIACS [email protected] Jon Whittle NASA Ames Research Center - QSS Group Inc [email protected] 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 AUT- OFILTER 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.