Ilya Sergey (UCL / 조교수)
Fast Synthesis of Programs that Alter Data Structures
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 the program synthesizer called SuSLik. 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 SuSLik, and report on the experience of using it to synthesize a series of benchmark programs manipulating with heap-based linked data structures.
Prof Ilya Sergey does research in the area of programming languages (PL), program analysis and formal verification. In recent years, He has mainly been concerned with developing scalable methods for building trustworthy concurrent and distributed software with application to consensus protocols and blockchains, but his earlier work was advancing the state of the art in static analysis for higher-order languages and PL design.
Prior to joining academia, Ilya has spent a part of his career in industry, working in JetBrains Inc., a world-leading company in creating integrated development environments for software developers. He obtained his PhD at KU Leuven (Belgium), and was a postdoctoral researcher at IMDEA Software Institute (Spain) and a Lecturer (Assistant Professor) at University College London (UK). He will be taking an appointment as a tenure-track Assistant Professor at Yale-NUS College (Singapore) starting November 2018.