Towards certifying domain-specific properties of synthesized code

G. Roşu; J. Whittle

doi:10.1109/ASE.2002.1115032

Towards certifying domain-specific properties of synthesized code

G. Roşu, J. Whittle

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

7 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 language	English
Title of host publication	Proceedings - ASE 2002
Subtitle of host publication	17th IEEE International Conference on Automated Software Engineering
Publisher	IEEE, Institute of Electrical and Electronics Engineers
Pages	289-294
Number of pages	6
ISBN (Electronic)	0769517366, 9780769517360
DOIs	https://doi.org/10.1109/ASE.2002.1115032
Publication status	Published - 1 Jan 2002
Externally published	Yes
Event	Automated Software Engineering Conference 2002 - Edinburgh, United Kingdom Duration: 23 Sept 2002 → 27 Sept 2002 Conference number: 17th

Publication series

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

Conference

Conference	Automated Software Engineering Conference 2002
Abbreviated title	ASE 2002
Country/Territory	United Kingdom
City	Edinburgh
Period	23/09/02 → 27/09/02

Access to Document

10.1109/ASE.2002.1115032

Cite this

Roşu, G., & Whittle, J. (2002). Towards certifying domain-specific properties of synthesized code. In Proceedings - ASE 2002: 17th IEEE International Conference on Automated Software Engineering (pp. 289-294). (Proceedings - ASE 2002: 17th IEEE International Conference on Automated Software Engineering). IEEE, Institute of Electrical and Electronics Engineers. https://doi.org/10.1109/ASE.2002.1115032

@inproceedings{f725a13510404277b623576ffad0e58f,

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",

month = jan,

day = "1",

doi = "10.1109/ASE.2002.1115032",

language = "English",

series = "Proceedings - ASE 2002: 17th IEEE International Conference on Automated Software Engineering",

publisher = "IEEE, Institute of Electrical and Electronics Engineers",

pages = "289--294",

booktitle = "Proceedings - ASE 2002",

address = "United States of America",

note = "Automated Software Engineering Conference 2002, ASE 2002 ; Conference date: 23-09-2002 Through 27-09-2002",

}

Roşu, G & Whittle, J 2002, Towards certifying domain-specific properties of synthesized code. in Proceedings - ASE 2002: 17th IEEE International Conference on Automated Software Engineering. Proceedings - ASE 2002: 17th IEEE International Conference on Automated Software Engineering, IEEE, Institute of Electrical and Electronics Engineers, pp. 289-294, Automated Software Engineering Conference 2002, Edinburgh, United Kingdom, 23/09/02. https://doi.org/10.1109/ASE.2002.1115032

Towards certifying domain-specific properties of synthesized code. / Roşu, G.; Whittle, J.
Proceedings - ASE 2002: 17th IEEE International Conference on Automated Software Engineering. IEEE, Institute of Electrical and Electronics Engineers, 2002. p. 289-294 (Proceedings - ASE 2002: 17th IEEE International Conference on Automated Software Engineering).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › Research › peer-review

TY - GEN

T1 - Towards certifying domain-specific properties of synthesized code

AU - Roşu, G.

AU - Whittle, J.

N1 - Conference code: 17th

PY - 2002/1/1

Y1 - 2002/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84982924085&partnerID=8YFLogxK

U2 - 10.1109/ASE.2002.1115032

DO - 10.1109/ASE.2002.1115032

M3 - Conference Paper

AN - SCOPUS:84982924085

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

SP - 289

EP - 294

BT - Proceedings - ASE 2002

PB - IEEE, Institute of Electrical and Electronics Engineers

T2 - Automated Software Engineering Conference 2002

Y2 - 23 September 2002 through 27 September 2002

ER -

Roşu G, Whittle J. Towards certifying domain-specific properties of synthesized code. In Proceedings - ASE 2002: 17th IEEE International Conference on Automated Software Engineering. IEEE, Institute of Electrical and Electronics Engineers. 2002. p. 289-294. (Proceedings - ASE 2002: 17th IEEE International Conference on Automated Software Engineering). doi: 10.1109/ASE.2002.1115032

Towards certifying domain-specific properties of synthesized code

Abstract

Publication series

Conference

Access to Document

Other files and links

Cite this