Deductive Synthesis of Programs that Alter Data Structures (KEYWORDS: Separation Logic, Program Synthesis, Proof Search)
COM1 Level 3
MR1, COM1-03-19
Abstract:
In my talk, I will describe a deductive approach for synthesizing imperative programs with pointers from declarative specifications expressed in Separation Logic. The approach treats logical program specifications, given in the form or pre- and postconditions with a pure and a spatial part, as proof goals, and provides an algorithm for rule-directed program construction based on the shape of the symbolic heap footprint a desired program manipulates.
The program synthesis algorithm rests on the novel framework of Synthetic Separation Logic (SSL), which generalises the classical notion of heap entailment P |- Q from Separation Logic to incorporate a possibility of transforming a heap satisfying an assertion P so the result would satisfy an assertion Q. A synthesized program represents a proof term for a transforming entailment statement P ~> Q, and the synthesis procedure corresponds to a proof search. The produced executable programs are, thus, correct by construction, in the sense that they satisfy the ascribed pre/postconditions, and are accompanied by complete proof derivations (i.e., certificates), which can be checked independently by a third-party verifier.
The approach has been implemented as a proof search engine for SSL in a form a program synthesizer. For efficiency, the engine exploits properties of SSL specifications, aggressively relying on a version of the Frame Rule and commutativity of separating conjunction to prune the search space. I will explain and showcase the use of SSL on characteristic examples, describe the design of our tool, and report on the experience of using it to synthesize a series of benchmark programs manipulating with heap-based linked data structures.
This is a joint work with Nadia Polikarpova (UC San Diego).
Biodata:
Ilya does research in programming language theory, including, but not limited to types, semantics, software verification, and program synthesis. Since November 2018, Ilya is a tenure-track Associate Professor at Yale-NUS College (Singapore). From November 2015 till October 2018, he was a faculty at the Department of Computer Science of University College London. Prior to joining UCL, from December 2012 to October 2015, he was a postdoc at IMDEA Software Institute. From November 2008 to November 2012, he was a research assistant in the CS Department of KU Leuven, where I obtained my PhD. Ilya got his MSc degree in Mathematics and CS in 2008 from Dept. of Mathematics and Mechanics of Saint Petersburg State University. Before joining academia, Ilya worked as a software developer at JetBrains.