Events Calendar

CS Colloquium: Nadia Polikarpova (MIT CSAIL) - Type-Driven Program Synthesis

Speaker: Nadia Polikarpova, MIT CSAIL

Talk Title: Type-Driven Program Synthesis

Series: CS Colloquium

Abstract: This lecture satisfies requirements for CSCI 591: Computer Science Research Colloquium.

Modern programming languages safeguard developers from many classes of common errors, yet more subtle errors-”such as violations of security policies-”still plague software. Program synthesis has the potential to eliminate such errors, by generating executable code from concise and intuitive high-level specifications. The major obstacle to practical program synthesis is in navigating large search spaces to find programs that satisfy a given specification. My work addresses this problem through the design of synthesis-friendly type systems that are able to decompose a synthesis problem into smaller problems and efficiently navigate the search space.

Based on this principle I developed Synquid, a synthesizer that generates programs from type-based specifications. Synquid is the first synthesizer to automatically discover provably correct implementations of sorting algorithms, as well as balancing and insertion operations on Red-Black Trees and AVL Trees. For these programs, the required specifications are up to seven times more concise than the implementations, and the synthesis times range from fractions of a second (for insertion sort) to under a minute (for Red-Black Tree rotations). Going beyond textbook algorithms, I creates a language called Lifty, which uses type-driven synthesis to automatically rewrite programs that violate information flow policies.

In our case study, Lifty was able to enforce all required policies in a prototype conference management system.


Biography: Nadia Polikarpova is a postdoctoral researcher at the MIT Computer Science and Artificial Intelligence Lab, interested in helping programmers build secure and reliable software. She completed her PhD at ETH Zurich. For her dissertation she developed tools and techniques for automated formal verification of object-oriented libraries, and created the first fully verified general-purpose container library, receiving the Best Paper Award at the International Symposium on Formal Methods. During her doctoral studies, Nadia was an intern at MSR Redmond, where she worked on verifying real-world implementations of security protocols. At MIT, Nadia has been applying formal verification to automate various critical and error-prone programming tasks.

Host: Chao Wang

Location: Ronald Tutor Hall of Engineering (RTH) - 217

Audiences: Everyone Is Invited

Contact: Assistant to CS chair