@InProceedings{CAV2017DecoratedSynthesis,
author="Gasc{\'o}n, Adri{\`a} and Tiwari, Ashish and Carmer, Brent and Mathur, Umang",
editor="Majumdar, Rupak
and Kun{\v{c}}ak, Viktor",
title="Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis",
booktitle="Computer Aided Verification",
year="2017",
publisher="Springer International Publishing",
address="Cham",
pages="86--103",
abstract="We introduce a technique for component-based program synthesis that relies on searching for a target program and its proof of correctness simultaneously using a purely constraint-based approach, rather than exploring the space of possible programs in an enumerate-and-check loop. Our approach solves a synthesis problem by checking satisfiability of an {\$}{\$}{\backslash}exists {\backslash}exists {\$}{\$}constraint {\$}{\$}{\backslash}phi {\$}{\$}, whereas traditional program synthesis approaches are based on solving an {\$}{\$}{\backslash}exists {\backslash}forall {\$}{\$}constraint. This enables the use of SMT-solving technology to decide {\$}{\$}{\backslash}phi {\$}{\$}, resulting in a scalable practical approach. Moreover, our technique uniformly handles both functional and nonfunctional criteria for correctness. To illustrate these aspects, we use our technique to automatically synthesize several intricate and non-obvious cryptographic constructions.",
isbn="978-3-319-63390-9"
}