We do research in the design and implementation of programming languages, program synthesis, and computer-assisted formal reasoning about complex systems, at the School of Computing of National University of Singapore, as a part of PLSE@NUS lab.

Announcements

We are actively looking for motivated PhD students! Get in touch with Ilya Sergey if you want to chat about research opportunities, and apply here.

Research internships: In case if you are interested in an internship with us, please get in touch with your CV and a paragraph of text describing your specific interests in the research themes we pursue at the moment. Strong background in PL/logic/verification or systems-building is a must. Prospective internship candidates will have to complete a test verification task.

Most of research done in the lab for now is powered by Lean proof assistant.

Our current investigations follow the themes outlined below. For more details on our research, check out our projects, and recent papers.

Theme 1: Verified Software Systems

Given the importance of modern software systems (e.g., distributed systems, concurrency and high-performance computing libraries, etc) and their complexity, it is vital in industry to have a rigorous verification methodology for establishing their correctness properties as well as for making sure that the once completed proofs don’t go “bit rot”. In this line of work, our recent work has introduced logical foundations for compositional verification of complex distributed protocols using a proof assistant. We have also produced the first mechanically verified proof of safety of Nakamoto consensus, its probabilistic properties and verified libraries of relevant probabilistic data structures. We also explored techniques for both foundational and lightweight verification of distributed systems. Finally, we have developed the first approach for (mostly) automated evolution of proofs for verified libraries.

Our long-term goal is to build verification tools that bridge the gap between the systems implementations and their abstract models that can be verified in an interactive or automated fashion, producing robust and easy-to-maintain proofs.

Theme 2: Program Synthesis with Correctness Guarantees

Program synthesis is an emerging research and technology paradigm for automatically deriving programs from user-provided declarative specifications, thereby significantly reducing the implementation effort required for producing correct-by-construction and efficient code. Our recent work explored the marriage of state-of-the-art techniques for deductive proofs in a proof assistants (e.g., Coq and Lean) and program synthesis that resulted in a series of tools that produce correct-by construction implementations for complex tasks in mainstream languages, as well as approaches for automatically synthesisng data structure specifications.

Our long-term agenda targets synthesis of provably correct high-performance, safety-critical programs with the focus on low-effort proof automation and evolution.

Theme 3: Foundations of Verified Program Generation

Often, it is not easy capture an intent of a program synthesis task with a specification that can be also used to formally verify that the synthesised program is indeed correct. In our recent work we started to approach instances of program synthesis with such “intuitive but tricky to make formal” specifications, including generation of sparse data manipulations and automated exploit discovery, from the perspective of program logics.

Our vision in this line of work is to push the state of the art in what can be specified and synthesised, by developing expressive formalisms that capture the program synthesis intent and allow one to mechanically verify its result, interactively or automatically.