Automated program synthesis is an area that has recently attracted a lot of interest in industry and academia. With modern machine learning-powered synthesis tools, such as GitHub Copilot, it seems that fully automated generation of code based on programmer’s intent is almost within our reach. But can we really trust that the code produced by the machine does exactly what is intended and will not break in subtle corner cases—the problem known as overfitting? It would be nice, if, along the synthesised code, we could have a formal proof that the code is safe to run and satisfies a specification ascribed by the programmer in a sufficiently expressive logic, thus eliminating any possibility of its erroneous behaviour.

In this talk, I will describe an approach allowing one to build a certified program synthesiser that can generate provable-correct imperative program in a C-like language from user-provided pre- and post-conditions. We will touch upon some basic ideas of Hoare-style program verification, separation logic, and interactive theorem proving, culminating with an overview of SuSLik—an automated tool that synthesises heap-manipulated programs together with machine-checkable proofs of their correctness.

I am a tenured Associate Professor at National University of Singapore and Yale-NUS College. I do research in programming language design and implementation, software verification, distributed systems, program synthesis and repair. I am the recipient of the AITO Dahl-Nygaard Junior Prize 2019. I designed and co-developed Scilla, a programming language for safe smart contracts, used by Zilliqa. I organised the ICFP Programming Contest 2019.

Before moving to Singapore, I was a faculty at University College London in 2015-2018. Prior to that, I was a postdoc at IMDEA Software Institute. I hold a PhD in Computer Science from KU Leuven, and an MSc in mathematics from St Petersburg University. Before joining academia I worked as a software engineer at JetBrains.