Program Synthesis Using Dual Interpretation

Ashish Tiwari; Adrià  Gascón; Bruno Dutertre

doi:10.1007/978-3-319-21401-6_33

Program Synthesis Using Dual Interpretation

Ashish Tiwari, Adrià Gascón, Bruno Dutertre

School of Informatics

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We present an approach for component-based program synthesis that uses two distinct interpretations for the symbols in the program. The first interpretation defines the semantics of the program. It is used to specify functional requirements. The second interpretation is used to capture nonfunctional requirements that may vary by application. We present a language for program synthesis from components that uses dual interpretation. We reduce the synthesis problem to an exists-forall problem, which is solved using the exists-forall extension of the SMT-solver Yices. We use our approach to synthesize bitvector manipulation programs, padding-based encryption schemes, and block cipher modes of operations.

Original language	English
Title of host publication	25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings
Editors	P. Amy Felty, Aart Middeldorp
Publisher	Springer
Pages	482-497
Number of pages	16
ISBN (Electronic)	978-3-319-21401-6
ISBN (Print)	978-3-319-21400-9
DOIs	https://doi.org/10.1007/978-3-319-21401-6_33
Publication status	Published - 2015

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer International Publishing
Volume	9195
ISSN (Print)	0302-9743

Access to Document

10.1007/978-3-319-21401-6_33

cade2015Accepted author manuscript, 374 KB

http://link.springer.com/chapter/10.1007%2F978-3-319-21401-6_33

Cite this

@inproceedings{ad70022cf2704cb0931edbdaa95af9f3,

title = "Program Synthesis Using Dual Interpretation",

abstract = "We present an approach for component-based program synthesis that uses two distinct interpretations for the symbols in the program. The first interpretation defines the semantics of the program. It is used to specify functional requirements. The second interpretation is used to capture nonfunctional requirements that may vary by application. We present a language for program synthesis from components that uses dual interpretation. We reduce the synthesis problem to an exists-forall problem, which is solved using the exists-forall extension of the SMT-solver Yices. We use our approach to synthesize bitvector manipulation programs, padding-based encryption schemes, and block cipher modes of operations.",

author = "Ashish Tiwari and Adri{\`a} Gasc{\'o}n and Bruno Dutertre",

year = "2015",

doi = "10.1007/978-3-319-21401-6\_33",

language = "English",

isbn = "978-3-319-21400-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "482--497",

editor = "Felty, \{P. Amy\} and Aart Middeldorp",

booktitle = "25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings",

address = "United Kingdom",

}

Program Synthesis Using Dual Interpretation. / Tiwari, Ashish; Gascón, Adrià ; Dutertre, Bruno.
25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. ed. / P. Amy Felty; Aart Middeldorp. Springer, 2015. p. 482-497 (Lecture Notes in Computer Science; Vol. 9195).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Program Synthesis Using Dual Interpretation

AU - Tiwari, Ashish

AU - Gascón, Adrià

AU - Dutertre, Bruno

PY - 2015

Y1 - 2015

N2 - We present an approach for component-based program synthesis that uses two distinct interpretations for the symbols in the program. The first interpretation defines the semantics of the program. It is used to specify functional requirements. The second interpretation is used to capture nonfunctional requirements that may vary by application. We present a language for program synthesis from components that uses dual interpretation. We reduce the synthesis problem to an exists-forall problem, which is solved using the exists-forall extension of the SMT-solver Yices. We use our approach to synthesize bitvector manipulation programs, padding-based encryption schemes, and block cipher modes of operations.

AB - We present an approach for component-based program synthesis that uses two distinct interpretations for the symbols in the program. The first interpretation defines the semantics of the program. It is used to specify functional requirements. The second interpretation is used to capture nonfunctional requirements that may vary by application. We present a language for program synthesis from components that uses dual interpretation. We reduce the synthesis problem to an exists-forall problem, which is solved using the exists-forall extension of the SMT-solver Yices. We use our approach to synthesize bitvector manipulation programs, padding-based encryption schemes, and block cipher modes of operations.

U2 - 10.1007/978-3-319-21401-6_33

DO - 10.1007/978-3-319-21401-6_33

M3 - Conference contribution

SN - 978-3-319-21400-9

T3 - Lecture Notes in Computer Science

SP - 482

EP - 497

BT - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings

A2 - Felty, P. Amy

A2 - Middeldorp, Aart

PB - Springer

ER -

Program Synthesis Using Dual Interpretation

Abstract

Publication series

Access to Document

Fingerprint

Cite this