Current Research Affiliates
Former Group Members
Graduated PhD Students
- Kiran Gopinathan, PhD Student, NUS School of Computing, 2019-2024.
PhD Thesis: Scaling the Evolution of Verified Software, August 2024
First appointment: Postdoctoral Researcher at University of Illinois Urbana-Champaign
Former Postdocs
- Thibault Dardinier, Visiting Research Fellow, NUS, November-December 2025
- Yutaka Nagashima, Postdoctoral Researcher, NUS, December 2020-January 2022
- Thomas Sibut-Pinote, Research Associate, UCL, November 2017-August 2018
Graduated MSc Students
- Tram Hoang, MComp student at NUS School of Computing, AY 2021/22.
Testing Static Program Analyses with a State-Collecting Monadic Definitional Interpreter. [Thesis] - Bryan Tan Yao Hong, MComp student at NUS School of Computing, AY 2021/22.
From C towards Idiomatic & Safer Rust through Constraints-Guided Refactoring. [Thesis | Code] - Yasunari Watanabe, MComp student at NUS School of Computing, AY 2020/21.
A Framework for Certified Program Synthesis. [Thesis | Code] - George Pîrlea, MEng student at UCL, AY 2018/19.
Toychain: Formally Verified Blockchain Consensus. [Thesis | Code]
Graduated Final-Year Project Advisees
- Callista Le, Capstone student at Yale-NUS College, AY 2023/24.
Simple and Efficient Concurrent Data Structures via Batch Parallelism. [Thesis]
- Nay Chi Wint Naing, Capstone student at Yale-NUS College, AY 2023/24.
Program Synthesis with Accumulators. [Thesis]
- Sewen Thy, Capstone student at Yale-NUS College, AY 2022/23.
Borrowing without Sorrowing: Implementing Extract Method Refactoring for Rust. [Thesis]
🏆 Recipient of Outstanding Yale-NUS Capstone Prize for 2023 - Karolina Grzeszkiewicz, Capstone student at Yale-NUS College, AY 2022/23.
Formally Verifying Accountable Byzantine Consensus. [Thesis]
- Koon Wen Lee, Capstone student at Yale-NUS College, AY 2022/23.
Concurrent Structures and Effect Handlers: A Batch Made in Heaven. [Thesis]
- Mayank Keoliya, FYP student at NUS School of Computing, AY 2022/23.
Improving Rust Performance by Type-Directed Refactoring.
- Theodore Leebrant, FYP student at NUS School of Computing, AY 2022/23.
Improving Rust Performance by Type-Directed Refactoring.
- Mark Weilong Yuen, Capstone student at Yale-NUS College, AY 2021/22.
Verifying Distributed Protocols: From Executable to Decidable. [Thesis]
- Juwon Lee, Capstone student at Yale-NUS College, AY 2021/22.
Synthesizing Musical Harmony using Equality Graphs. [Thesis]
- Tram Hoang, Capstone student at Yale-NUS College, AY 2020/21.
Testing Static Code Analyses with Monadic Definitional Interpreters. [Thesis]
- Bryan Tan Yao Hong, Capstone student at Yale-NUS College, AY 2020/21.
Towards Enhancing Deductive Synthesis of Heap-Manipulating Programs with Examples. [Thesis]
- Nicholas Chin Jian Wei, Capstone student at Yale-NUS College, AY 2020/21.
Towards Locally-Parallel Processing of Smart Contract Transactions. [Thesis]
- Alaukik Nath Pant, Capstone student at Yale-NUS College, AY 2020/21.
Towards User-Friendly Linearizability Checking. [Thesis]
- Gabriel Petrov, Capstone student at Yale-NUS College, AY 2020/21.
A Study of Control and Type-Flow Analyses for Higher-Order Programming Languages. [Thesis]
- Yasunari Watanabe, Capstone student at Yale-NUS College, AY 2019/20.
Building a Certified Program Synthesizer. [Thesis]
🏆 Recipient of Outstanding Yale-NUS Capstone Prize for 2020 - Jake (Si Yuan) Goh, Capstone student at Yale-NUS College, AY 2018/19.
Synchronisation Primitives for Smart Contracts. [Thesis] - Daniel Lok, Capstone student at Yale-NUS College, AY 2018/19.
Modelling and Testing Composite Byzantine-Fault Tolerant Consensus Protocols. [Thesis] - Anirudh Pillai, UCL, Undergraduate student, AY 2017/18
Mechanised Verification of Paxos-like Consensus Protocols. [BSc Thesis]
Interns and Visiting Students
- Gokul Rajiv, Research Assistant at NUS SoC, 2024-2026.
Project: Programming Language Synthesis for Automated Exploit Generation [Paper] - Ziyu Mao, Research Intern at NUS SoC, August 2025–March 2026
Project: Implementing a Certified Model Checker in Lean - Vitaly Kurin, Research Intern at NUS SoC, June–October 2025
Project: Velvet: A Multi-Modal Verifier in Lean [Paper] - Vikram Goyal, Research Intern at NUS SoC, Spring 2024–Spring 2025
Project: Tackling Brittleness in SMT Proofs [Paper] - Elad Kinsbruner, Research Intern at NUS SoC, October 2024–March 2025.
Project: Verifying Distributed Protocols in Veil [Paper] - Sean Wang, Research Intern at NUS SoC, June–October 2024.
Project: Implementing a Relational Separation Logic in Lean - Mayank Keoliya, Research Intern at NUS SoC, Summer 2022–Spring 2023.
Project: Invariant Synthesis for Automated Proof Repair [Paper] [In the news]
🏆 Recipient of NUS Outstanding Undergraduate Researcher Prize for 2023 - Irina Artemeva, Research Intern at Yale-NUS College/NUS SoC, September-December 2020.
- Amy Zhu, Research Intern at Yale-NUS College/NUS SoC, Spring-Summer 2019.
Project: Synthesis of Heap-Manipulating Programs with Immutable Specifications [Paper] - Bryan Tan, Research Intern at Zilliqa, Summer 2019.
Project: Compilation of Scilla Smart Contract to SMT - Kiran Gopinathan, Intern, UCL, Summer 2018.
Project: Mechanising Probabilistic Properties of a Blockchain [Code | Paper] - Oscar King, Intern, UCL, Summer 2018.
Project: Code Extraction for Verified Blockchain Protocol - Kristoffer Just Arndal Andersen, Visiting PhD Researcher from Aarhus University, 2018, UCL.
Project: Distributed Protocol Combinators [Paper] - George Pîrlea, Intern, UCL, Summer 2017.
Project: Reasoning about blockchain consensus protocols. [Code | Paper] - Benedict Loh, Intern, UCL, Summer 2017.
Project: Program synhesis engine via Separation Logic. - Georgi Georgiev, Intern, UCL, Summer 2016.
Project: Parameterised verification of a concurrent garbage collector in Coq. [Code] - Anton Podkopaev, Intern, IMDEA Software Institute, Summer 2015.
Project: Operational Semantics for C/C++11 concurrency. [Code | Draft]