In this talk I will present a program synthesizer SuSLik, which accepts a separation logic specification as input, and produces a provably safe program as output. SuSLik is the first synthesizer capable of generating a wide range of operations on linked data structures (such as singly- and doubly-linked lists, sorted lists, and trees) without additional hints form the user. To make this possible, SuSLik relies on a novel proof system—synthetic separation logic—to derive correct-by-construction programs directly from their specifications.

Nadia Polikarpova is an Assistant Professor in the Computer Science and Engineering Department at the University of California, San Diego. She completed her PhD in 2014 at ETH Zurich (Switzerland) under the supervision of Bertrand Meyer. After that, she spent almost three years as a postdoc at MIT CSAIL, working with Armando Solar-Lezama. Her research interests span the areas of programming languages and formal methods; in particular, she is interested in building practical tools and techniques that make it easier for programmers to construct secure and reliable software.