Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis

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 $\exists\exists$ constraint $\phi$, whereas traditional program synthesis approaches are based on solving an $\exists\forall$ constraint. This enables the use of SMT-solving technology to decide $\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.