In this talk Ilya will provide an overview of a deductive approach for automatically synthesising 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.
Ilay and his team implemented this approach in a program synthesis tool called SuSLik. Ilay 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. He 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 MSc at St Petersburg University and PhD at KU Leuven. Before joining NUS, he was a postdoctoral researcher at IMDEA Software Institute and a faculty at University College London. Prior to starting an 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, Yale-NUS Distinguished Researcher award, as well as of research awards from Google, Facebook, and Amazon.
This will be a hybrid event in which Ilya gives his presentation in the lecture hall downstairs (0.05 Hoersaal), but we will also stream via Zoom.