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 ∃∃ constraint φ, whereas traditional program synthesis approaches are based on solving an ∃∀ constraint. This enables the use of SMT-solving technology to decide φ, resulting in a scalable practical approach. Moreover, our technique uniformly handles both functional and nonfunc-tional criteria for correctness. To illustrate these aspects, we use our technique to automatically synthesize several intricate and non-obvious cryptographic constructions.