Write a Blog >>
Mon 20 Jan 2020 15:35 - 16:40 at Conde - Closing Session

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.

Mon 20 Jan

Displayed time zone: Saskatchewan, Central America change

15:35 - 17:45
Closing SessionADSL at Conde
Programs Synthesis with Separation Logic
Nadia Polikarpova University of California, San Diego
Local Reasoning for Global Graph Properties
Thomas Wies New York University