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.
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!
Our work on higher-order specifications for deductive synthesis in SuSLik will appear at ECOOP’24.
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 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 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 Coq proof assistant and program synthesis that resulted in a series of foundational mechanisms and 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 programs with the focus on low-effort proof automation and evolution.
Despite being one of the oldest topics in Computer Science, concurrent programming still poses multiple challenges from both theoretical and practical standpoint: concurrent libraries that utilise available opportunities for parallelism are difficult to implement, optimise, and verify, and bugs in concurrent programs are extremely tricky to identify and fix. To address these challenges, we have developed foundations for machine-assisted verification of concurrent programs. We have also contributed tools for fast compositional bug-funding in concurrent code with theoretical completeness guarantees, and developed a methodology for efficient repair of concurrent bugs. We used the ideas from static program analysis and type systems to improve system-wide parallelism in modern blockchain protocols and applied advanced functional programming techniques to reduce the costs of building concurrent software.
Our vision in this line of work is to democratise the process implementation of concurrent libraries and applications, developing robust and accessible methods for building correct and performant concurrent programs.
Mechanised Separation Logic for Compositional Verification of Distributed Protocols
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.
Mechanised Hypersafety Proofs about Structured Data
2024 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2024). Copenhagen, Denmark, June 2024.
Simple and Efficient Concurrent Data Structures via Batch Parallelism
Capstone Thesis. Yale-NUS College, 2024.
Small Scale Reflection for the Working Lean User
Unpublished draft. 2024.
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2024). London, UK, January 2024. Distinguished Paper Award.