Skip directly to: content | search

ExCAPE: Expeditions in Computer Augmented Program Engineering

Syntax-Guided Synthesis Modulo Theories

PIs: Alur (Penn), Bodik (UC Berkeley), Martin (Penn), Seshia (UC Berkeley), and Solar Lezama (MIT)

The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on program synthesis and program optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementation.

In this collaborative effort we have defined a logic-based core computational problem so that different algorithmic strategies can be compared in an experimentally rigorous manner and computational advances can be easily shared across tools (such as Sketch and Transit). Based on this definition, we have organized a solvers competition SyGuS-COMP held at FLoC 2014.


Papers:

ExCAPE: Expeditions in Computer Augmented Program Engineering NSF National Science Foundation Award CCF-1138996