Colloquium – Ilya Sergey
October 18 @ 3:30 pm - 4:30 pm
Ilya Sergey
National University of Singapore
October 18, 2024
3:30 – 4:30 PM
Location: 3147 MEB (LCR)
Deductive Synthesis of Programs with Pointers: Expressive, Trustworthy, Fast
Abstract:
In this talk, I will provide an overview of an approach for automatically synthesizing imperative pointer-manipulating programs from declarative formal specifications.
The approach treats synthesis tasks, given in the form or logical pre- and postconditions, as proof goals, and the synthesis itself—as a proof search. The resulting synthesis algorithm produces executable programs in C that are correct by construction, in the sense that they satisfy the ascribed specifications and are accompanied by proof certificates, which can be checked independently by a third-party verifier. The algorithm has been implemented in a program synthesis tool called SuSLik. I will explain and showcase SuSLik on characteristic examples, describe its design, and report on the experience of using it to synthesise many non-trivial programs that manipulate heap-based linked data structures. I will also talk about some recent advances of automatically certifying programs synthesised by SuSLik in the Coq proof assistant.
Bio:
Ilya Sergey is an Associate Professor at the School of Computing of National University of Singapore, where he leads the Verified Systems Engineering lab. Ilya got his PhD in Computer Science at KU Leuven. Before joining NUS, he was a postdoctoral researcher at IMDEA Software Institute and a faculty at University College London. Prior to becoming an academic, he worked as a software developer at JetBrains.
Ilya does research in programming language design and implementation, distributed systems, software verification, and program synthesis. He is a recipient of several distinguished paper awards at POPL and PLDI, the 2019 Dahl-Nygaard Junior Prize, Yale-NUS Distinguished Researcher award, and academic research awards from Google, Facebook, and Amazon.