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.

• Type: Journal
• Year: 2015
• Where: CADE
• Authors: Ashish Tiwari, Adria Gascón, Bruno Dutertre
• Keywords: CADE 2015, Logical Reasoning