Publications
Recent
Foundational Multi-Modal Program Verifiers
53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2026). Rennes, France, January 2026.
Velvet: A Multi-Modal Verifier for Effectful Programs
Dafny Workshop 2026 (co-located with POPL 2026). Rennes, France, January 2026.
Lessons from Building an Auto-Active Verifier in Lean
Dafny Workshop 2026 (co-located with POPL 2026). Rennes, France, January 2026.
Inductive Synthesis of Inductive Heap Predicates
40th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2025). Singapore, October 2025.
Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference
41st International Conference on Logic Programming (ICLP 2025). Rende, Italy, September 2025.
Sound and Efficient Generation of Data-Oriented Exploits via Programming Language Synthesis
34th USENIX Security Symposium. Seattle, WA, USA, August 2025.
Veil: A Framework for Automated and Interactive Verification of Transition Systems
37th International Conference on Computer Aided Verification (CAV 2025). Zagreb, Croatia, July 2025.
Accelerating Automated Program Verifiers by Automatic Proof Localization
37th International Conference on Computer Aided Verification (CAV 2025). Zagreb, Croatia, July 2025.
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.
Greybox Fuzzing of Distributed Systems
30th ACM Conference on Computer and Communications Security (CCS 2023). Copenhagen, Denmark, December 2023.
Adventure of a Lifetime: Extract Method Refactoring for Rust
38th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2023). Lisbon, Portugal, October 2023.
Mostly Automated Proof Repair for Verified Libraries
2023 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023). Orlando, FL, USA, June 2023. ACM SIGPLAN Distinguished Paper Award
Leveraging Rust Types for Program Synthesis
2023 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023). Orlando, FL, USA, June 2023. Distinguished Artifact Award
Borrowing without Sorrowing: Implementing Extract Method Refactoring for Rust
Capstone Thesis. Yale-NUS College, 2023. Recipient of the Outstanding Yale-NUS Capstone Prize for 2023.
Formally Verifying Accountable Byzantine Consensus
Capstone Thesis. Yale-NUS College, 2023.
Concurrent Structures and Effect Handlers: A Batch Made in Heaven
Capstone Thesis. Yale-NUS College, 2023.
HIPPODROME: Data Race Repair using Static Analysis Summaries
ACM Transactions on Software Engineering and Methodology. 2023.
Random Testing of a Higher-Order Blockchain Language (Experience Report)
27th ACM SIGPLAN International Conference on Functional Programming (ICFP 2022). Ljubljana, Slovenia, September 2022.
From C towards Idiomatic & Safer Rust through Constraints-Guided Refactoring
MComp Thesis. NUS School of Computing, 2022.
Synthesizing Musical Harmony using Equality Graphs
Capstone Thesis. Yale-NUS College, 2022.
Verifying Distributed Protocols: From Executable to Decidable
Capstone Thesis. Yale-NUS College, 2022.
A Lazy Desugaring System for Evaluating Programs with Sugars
16th International Symposium on Functional and Logic Programming (FLOPS 2022). Taking place virtually, May 2022.
The Next 700 Smart Contract Languages
Principles of Blockchain Systems 2021. Pages 69–94. Morgan & Claypool. Author’s version.
Certifying the Synthesis of Heap-Manipulating Programs
26th ACM SIGPLAN International Conference on Functional Programming (ICFP 2021). Taking place virtually, August 2021.
GopCaml: A Structural Editor for OCaml
2021 OCaml Users and Developers Workshop (OCaml 2021). Taking place virtually, August 2021.
Deductive Synthesis of Programs with Pointers: Techniques, Challenges, Opportunities (Invited Paper)
33rd International Conference on Computer-Aided Verification (CAV 2021). Taking place virtually, July 2021.
Practical Smart Contract Sharding with Ownership and Commutativity Analysis
2021 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2021). Taking place virtually, June 2021.
Cyclic Program Synthesis
2021 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2021). Taking place virtually, June 2021. ACM SIGPLAN Distinguished Paper Award.
A Framework for Certified Program Synthesis
MComp Thesis. NUS School of Computing, 2021.
Testing Static Code Analyses with Monadic Definitional Interpreters
Capstone Thesis. Yale-NUS College, 2021.
Towards Enhancing Deductive Synthesis of Heap-Manipulating Programs with Examples
Capstone Thesis. Yale-NUS College, 2021.
Towards User-Friendly Linearizability Checking
Capstone Thesis. Yale-NUS College, 2021.
A Study of Control and Type-Flow Analyses for Higher-Order Programming Languages
Capstone Thesis. Yale-NUS College, 2021.
Towards Locally-Parallel Processing of Smart Contract Transactions
Capstone Thesis. Yale-NUS College, 2021.
Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
22nd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2021). Copenhagen, Denmark, January 2021.
Protocol Combinators for Modeling, Testing, and Execution of Distributed Systems
Accepted for publication in Journal of Functional Programming in 2021. Cambridge University Press.
Building a Certified Program Synthesizer
Capstone Thesis. Yale-NUS College, 2020. Recipient of the Outstanding Yale-NUS Capstone Prize for 2020.
Compiling a Higher-Order Smart Contract Language to LLVM
2020 Virtual LLVM Developers’ Meeting on the LLVM Compiler Infrastructure, October 2020.
Certifying Certainty and Uncertainty in Approximate Membership Query Structures
32nd International Conference on Computer-Aided Verification (CAV 2020). Los Angeles, CA, USA, July 2020.
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
29th European Symposium on Programming (ESOP 2020). Dublin, Ireland, April 2020.
Safer Smart Contract Programming with Scilla
34th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2019). Athens, Greece, October 2019. Distinguished Artifact Award.
Toychain: Formally Verified Blockchain Consensus
MEng Thesis. University College London, 2019
Synchronisation Primitives for Smart Contracts
Capstone Thesis. Yale-NUS College, 2019.
Modelling and Testing Composite Byzantine-Fault Tolerant Consensus Protocols
Capstone Thesis. Yale-NUS College, 2019.
QED at Large: A Survey of Engineering of Formally Verified Software
Found. Trends Program. Lang. 2019. Vol. 5, (2-3), Pages 102–281.
Exploiting the laws of order in smart contracts
ISSTA 2019
Towards Mechanising Probabilistic Properties of a Blockchain
CoqPL 2019
Structuring the Synthesis of Heap-Manipulating Programs
46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019). Lisbon, Portugal, January 2019. ACM SIGPLAN Distinguished Paper Award
A True Positives Theorem for a Static Race Detector
46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019). Lisbon, Portugal, January 2019.
Finding The Greedy, Prodigal, and Suicidal Contracts at Scale
ACSAC 2018
RacerD: Compositional Static Race Detection
33rd ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 2018). Boston, MA, USA, November 2018.
Paxos Consensus, Deconstructed and Abstracted
ESOP. 2018
Mechanising Blockchain Consensus
7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2018). Los Angeles, CA, USA, January 2018.
Programming and Proving with Distributed Protocols
45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018). Los Angeles, CA, USA, January 2018.
A Concurrent Perspective on Smart Contracts
1st Workshop on Trusted Smart Contracts. 2017
Programming Language Abstractions for Modularly Verified Distributed Systems
SNAPL 2017
