Current Research Affiliates
Former Group Members
PhD Students and Postdocs
- Yutaka Nagashima, Postdoctoral Researcher, NUS, December 2020-January 2022.
- Maria A Schett, PhD student, UCL, November 2017-May 2019.
- Thomas Sibut-Pinote, Research Associate, UCL, November 2017-August 2018.
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]
Undergraduate and Capstone Advisees
- 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
- 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]