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.
Postdoc positions are available in a project on automated program repair via static analysis and verification. Check out the project page for the details and get in touch!
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. We welcome candidates who will commit six months or longer to focused research on-site.
Our current investigations follow the themes outlined below.
For more details on our research, check out our blog posts, projects, and recent papers.
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 Coq proof assistant and program synthesis that resulted in a series of tools that produce correct-by construction implementations for complex tasks in mainstream languages.
Our long-term agenda targets synthesis of provably correct high-performance, safety-critical systems with the focus on low-effort proof automation and evolution.
Given the importance of distributed systems and their complexity, it is vital in industry to have a rigorous verification methodology for establishing its correctness properties, ensuring that, once a distributed system is up and running, it will never go wrong and will eventually complete its goals. 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 lightweight verification of distributed systems, such as greybox fuzzing.
Our long-term goal is to build tools that bridge the gap between the systems implementations and their abstract models that can be verified in an interactive or automated fashion.
Congratulations to Mayank Keoliya on awarded the 2023 NUS Outstanding Undergraduate Researcher Prize!
Congratulations to Kiran Gopinathan on receiving a Dean's Research Excellence Award!
The paper on implementing Extract Method refactoring for Rust will appear at OOPSLA'23.
The paper on fuzzing distributed systems will appear at CCS'23.
The implementation of RusSOL has won a PLDI'23 Distinguished Artifact Award (single award given out of 67 submitted artifacts).
30th ACM Conference on Computer and Communications Security (CCS 2023). Copenhagen, Denmark, December 2023.
38th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2023). Lisbon, Portugal, October 2023.
2023 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023). Orlando, FL, USA, June 2023. ACM SIGPLAN Distinguished Paper Award
2023 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023). Orlando, FL, USA, June 2023. Distinguished Artifact Award
Capstone Thesis. Yale-NUS College, 2023. Recipient of the Outstanding Yale-NUS Capstone Prize for 2023.
Capstone Thesis. Yale-NUS College, 2023.
Capstone Thesis. Yale-NUS College, 2023.
ACM Transactions on Software Engineering and Methodology. 2023.
27th ACM SIGPLAN International Conference on Functional Programming (ICFP 2022). Ljubljana, Slovenia, September 2022.
MComp Thesis. NUS School of Computing, 2022.