Computer Augmented Program Engineering

Despite significant advances in programming languages and verification tools, programming
remains a tedious, error-prone, and expensive activity.  This talk surveys an emerging approach
to software design in  which a programmer and an automated program-synthesis tool collaborate
to generate software that meets its specification.  A programmer expresses her insights about the
design using synthesis artifacts of different kinds such as programs that may contain ambiguities,
declarative specifications of high-level requirements,  positive and negative examples of desired
behaviors, and optimization criteria for selecting among alternative implementations.
The synthesis tool composes these different views about the structure and functionality of the system
into a unified  concrete implementation using a combination of algorithmic techniques such as decision
procedures for constraint-satisfaction problems, iterative schemes for abstraction and refinement,
and data-driven learning. We will illustrate this approach using a number of projects, including one
at Penn focusing on design of cache coherence protocols from a mix of concrete and symbolic
execution scenarios.