Current Research Affiliates

Former Group Members

Graduated Postdocs

• 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 Fynal-Year Project Advisees

• 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

• 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]