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.
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.
Our paper on using Answer Set Programming for invariant inference will appear at ICLP’25.
Our paper on accelerating SMT-based program verifiers will appear at CAV’25.
A paper on synthesising Separation Logic predicates via Answer Set Programming is accepted at OOPSLA’25.
A paper on programming language synthesis for automated exploit generation is accepted at USENIX Security’25.
Congratulations to Yunjeong Lee and Ziyi Yang on receiving Research Achievement Awards!
A paper on the taxonomy of intents and mechanisms for DSL design in Racket is accepted at SLE’24.
Kiran Gopinathan has successfully defended her PhD thesis “Scaling the Evolution of Verified Software”. Congratulations, Dr. Gopinathan!
Two new papers at upcoming conferences in October 2024: on compositional verification of Byzantine protocols (CCS’24) and on building concurrent data structures via batch-parallelism (OOPSLA’24).
Congratulations to George Pîrlea on receiving a Dean’s Research Excellence Award for 2024!
Most of research done in the lab currently 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.
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 methodology that combines both lightweight validation techniques, such as fuzz-testing and model checking with deductive proofs, both automated and human-assisted. Reasoning tools that provide the full spectrum of such validation methodologies are referred to as multi-modal verifiers. In this line of work, we are focusing on building multi-modal verifiers for different kinds of domains (including distributed systems, security protocols, and general-purpose languages) on top of Lean proof assistant, advancing the state of the art in methodlogies for testing, specification and invariant inference, as well automated and interactive program verification.
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.
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.
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.
A framework for verifying distributed systems automatically and interactive in Lean
Mechanised Separation Logic for Compositional Verification of Distributed Protocols
Inductive Synthesis of Inductive Heap Predicates
40th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2025). Singapore, October 2025.
Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference
41st International Conference on Logic Programming (ICLP 2025). Rende, Italy, September 2025.
Sound and Efficient Generation of Data-Oriented Exploits via Programming Language Synthesis
34th USENIX Security Symposium. Seattle, WA, USA, August 2025.
Veil: A Framework for Automated and Interactive Verification of Transition Systems
37th International Conference on Computer Aided Verification (CAV 2025). Zagreb, Croatia, July 2025.
Accelerating Automated Program Verifiers by Automatic Proof Localization
37th International Conference on Computer Aided Verification (CAV 2025). Zagreb, Croatia, July 2025.
Concurrent Data Structures Made Easy
39th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2024). Pasadena, CA, USA, October 2024.
DSLs in Racket: You Want It How, Now?
17th ACM SIGPLAN International Conference on Software Language Engineering (SLE ’24). Pasadena, CA, USA, October 2024.
Compositional Verification of Composite Byzantine Protocols
31st ACM Conference on Computer and Communications Security (CCS 2024). Salt Lake City, UT, USA, October 2024.
Higher-Order Specifications for Deductive Synthesis of Programs with Pointers
38th European Conference on Object-Oriented Programming (ECOOP 2024). Vienna, Austria, September 2024.
Scaling the Evolution of Verified Software
PhD Thesis. NUS School of Computing, August 2024.