Keynote Speaker

Ilya Sergey

Ilya is an Associate Professor at the School of Computing of National University of Singapore, where he leads the Verified Systems Engineering lab. He also holds a joint appointment at Yale-NUS College and is a lead language designer at Zilliqa, a Singapore FinTech start-up.

Ilya received his MSc from St Petersburg University and PhD from KU Leuven. Before joining NUS, he was a postdoctoral researcher at IMDEA Software Institute and a faculty at University College London. Prior to starting his academic career, he worked as a software developer at JetBrains.

Ilya does research in programming language design and implementation, software verification, distributed systems, program synthesis and repair. He is a recipient of distinguished paper awards at POPL and PLDI, the 2019 Dahl-Nygaard Junior Prize, the 2021 Yale-NUS Distinguished Researcher Award, and a Google Faculty Research Award.

Title

Deductive Synthesis of Heap-Manipulating Programs: Sound, Expressive, Fast

Abstract:

In my talk, I will describe a deductive approach for synthesising 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). The produced executable programs are correct by construction, in the sense that they satisfy the ascribed specifications, 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 synthesiser. 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 out tool, and report on the experience of using it to synthesise a series of benchmark programs manipulating with heap-based linked data structures. I will also tell about some recent advances of automatically certifying synthesised programs in the Coq proof assistant.