Seminars

Diversely Enumerating Solutions to Synthesis Problems PDF
Ethan Jackson, Microsoft Research

11/15/2013, 11:00am, GHC 7501

Abstract

Many synthesis problems reduce to a common task: Find a structure (e.g. an AST, a finite relation, etc...) with a certain property. It is well-known that constraint solvers are useful for solving this task. The approach is to encode (1) a space of structures with a set of variables and (2) a property as a set of constraints over these variables. However, constraint-based specifications may have (infinitely) many solutions, of which only a few might correspond to distinct solutions to the original synthesis problem. (For example, there are many equivalent programs that differ only by renaming of identifiers.) Consequently, a solver may enumerate many equivalent solutions before visiting a new part of the solution space. Or, it may enumerate distinct solutions in a highly biased manner.

In this talk I present theory and algorithms for better enumeration of solutions using modern constraint solvers. The goal is to first formalize solution enumerators and enumeration bias, and then build algorithms that decrease enumeration bias with modifying the underlying constraint solver. I define an "ideal diverse enumerator" as one that uniformly draws equivalence classes of solutions. Next, I present an algorithm, called "symmetry-directed randomized partitioning", for building empirically diverse enumerators from modern unmodified constraint solvers. Finally, I show that our diverse enumerator is significantly closer to the ideal compared to baseline and randomized solvers.

Biography

Ethan K. Jackson is a Researcher in The Research in Software Engineering (RiSE) Group at Microsoft Research. His work focuses on next-generation formal specification languages for model-based development with an emphasis on automated synthesis. He is the developer of the FORMULA language, which has been applied to software, cyber-physical, and biological systems. Ethan received his PhD in Computer Science from Vanderbilt University in 2007 and his BS in Computer Engineering from the University of Pittsburgh in 2004. He joined Microsoft Research in 2007.

http://research.microsoft.com/en-us/um/people/ejackson/