Thursday, April 7, 2016 - 3:00pm to 4:00pm
Location:Traffic 21 Classroom 6501 Gates & Hillman Centers
Speaker:NADIA POLIKARPOVA, Postdoctoral Associate http://people.csail.mit.edu/polikarn/
The key to scalable program synthesis is modular verification: the better a specification for a program can be broken up into independent specifications for its components, the fewer combinations of components the synthesizer has to consider, leading to a combinatorial reduction in the size of the search space. This talk will present Synquid: a synthesizer that takes advantage of the modularity offered by type-based verification techniques to efficiently generate recursive functional programs that provably satisfy a given specification in the form of a refinement type.
We have evaluated Synquid on a large set of synthesis problems and found that it exceeds the state of the art in terms of both scalability and usability. Synquid was able to synthesize more complex programs than those reported in prior work (for example, various sorting algorithms, operations on balanced trees). It was also able to handle most of the benchmarks tackled by existing tools, often starting from a significantly more concise and intuitive user input. Moreover, due to automatic refinement discovery through a variant of liquid type inference, our approach fundamentally extends the class of programs for which a provably correct implementation can be synthesized without requiring the user to provide full inductive invariants.
Nadia Polikarpova is a postdoc at MIT CSAIL, where she works on program synthesis with Armando Solar-Lezama. She completed her PhD in 2014 at ETH Zurich (Switzerland), under the supervision of Bertrand Meyer. Apart from program synthesis, Nadia is interested in automated deductive verification and security.
Faculty Host: Jan Hoffman