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

摘要

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 {exist}{exist} constraint Φ, whereas traditional program synthesis approaches are based on solving an {exist}{arbitrary} 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 nonfunctional criteria for correctness. To illustrate these aspects, we use our technique to automatically synthesize several intricate and non-obvious cryptographic constructions.