Sciweavers

Share
CADE
2015
Springer

Program Synthesis Using Dual Interpretation

4 years 7 months ago
Program Synthesis Using Dual Interpretation
Abstract. We present an approach to 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 solver of the SMT-solver Yices. We use our approach to synthesize bitvector manipulation programs, padding-based encryption schemes, and block cipher modes of operations.
Ashish Tiwari, Adria Gascón, Bruno Dutertre
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where CADE
Authors Ashish Tiwari, Adria Gascón, Bruno Dutertre
Comments (0)
books