Send email Copy Email Address

2023-03-17
 

Ilya Sergey from the School of Computing of National University of Singapore

Ilya Sergey will give a talk on "Deductive Synthesis of Programs with Pointers: Expressive, Trustworthy, Fast", Friday, 17th of March, at 10am

 

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.