I am a tenured Associate Professor at the School of Computing of National University of Singapore, where I run the VERSE research group as a part of PLSE@NUS lab. I also hold a joint appointment at Yale-NUS College.
I do research in programming language design and implementation, software verification, distributed systems, program synthesis and repair. I am the recipient of the AITO Dahl-Nygaard Junior Prize 2019. I designed and co-developed Scilla, a programming language for safe smart contracts, used by Zilliqa. I organised the ICFP Programming Contest 2019. In the past, I contributed to Facebook Infer and Glasgow Haskell Compiler. Very long time ago, I used to work on Scala and Clojure language support in IntelliJ IDEA.
Before moving to Singapore, I was a faculty at University College London in 2015-2018. Prior to that, I was a postdoc at IMDEA Software Institute. I hold a PhD in Computer Science from KU Leuven, and an MSc in mathematics from St Petersburg University. Before joining academia I worked as a software engineer at JetBrains.
School of Computing, National University of Singapore
COM1, 13 Computing Drive, Singapore 117417
||COM3-02-56 (NUS SoC); RC3-01-03E, Cendana (Yale-NUS College)|
|Office Phone:||+65 6516 1903|
- Multiple postdoc positions are available in the 5-year MOE Tier 3 project on automated program repair via static analysis and verification. Check out the project page for the details and get in touch!
- I am actively looking for motivated PhD students who would like to work on software analysis, verification, and certified synthesis, applying those techniques to concurrent and distributed systems. Feel free to email me if you'd like to chat about research opportunities and apply here. The next application deadline is 15 June 2023.
|Sep 21, 2022||I am thrilled to participate in the Workshop on Dependable and Secure Software Systems that will take place at ETH Zurich on October 7-8. I will present our work on sharding smart contracts.|
|Jul 20, 2022||I’m delighted to be amongst the recipients of the Fall 2021 Amazon Research Award.|
|Jul 18, 2022||Vladimir Gladstein joins VERSE lab as a PhD student. Welcome, Vladimir!|
|Jul 1, 2022||Our paper on random testing of Scilla interpreter and compiler with QuickChick (co-authored with Tram Hoang, Anton Trunov, and Leonidas Lampropoulos) will appear at ICFP’22.|
|Jun 20, 2022||Our paper on Hippodrome, a new tool for automated repair of concurrent data races, built on top of Infer Static Analyser, will appear at ACM Transactions on Software Engineering and Methodology. This is a joint work with Andreea Costea, Abhishek Tiwari, Sigmund Chianasta, Kishore R, and Abhik Roychoudhury.|
|Apr 5, 2022||I am chairing the Programme Committee of The 20th Asian Symposium on Programming Languages and Systems (APLAS 2022), which will take place on 5-10 December 2022 in Auckland, New Zealand (co-located with OOPSLA 2022). Submit your papers on programming languages, formal methods, verification tools, and systems! Deadline is 16 June 2022, AoE.|
|Sep 1, 2021||Ziyi Yang joins VERSE lab as a PhD student, and Tram Hoang and Bryan Tan join as MComp students. Welcome, Bryan, Tram, and Ziyi!|
|Aug 4, 2021||I am looking for postdocs to work on Certified Automated Program Repair. Check out the project page and get in touch!|
- Cyclic Program SynthesisPLDI 2021. Pages 944–959. ACM.PLDI 2021 Distinguished Paper Award
- Practical Smart Contract Sharding with Ownership and Commutativity AnalysisPLDI 2021. Pages 1327–1341. ACM.
- Certifying Certainty and Uncertainty in Approximate Membership Query StructuresCAV 2020. LNCS, Vol. 12225, Pages 279–303. Springer.
- Safer Smart Contract Programming with ScillaProc. ACM Program. Lang. 2019. Vol. 3, (OOPSLA), Pages 185:1–185:30. ACM.OOPSLA 2019 Distinguished Artifact Award
- Structuring the Synthesis of Heap-Manipulating ProgramsProc. ACM Program. Lang. 2019. Vol. 3 (POPL), Pages 72:1–72:30. ACM.POPL 2019 Distinguished Paper Award
- Programming and Proving with Distributed ProtocolsProc. ACM Program. Lang. 2018. Vol. 2 (POPL), Pages 28:1–28:30. ACM.
Programs and Proofs: Mechanizing Mathematics with Dependent TypesLecture notes with exercises.
Last time I checked, my Erdős number was 4.
Here is a high-resolution "official" photo of me, suitable for
appropriate occasions. Just in case, here's a more casual picture, couresy of
Elena Alhimovich. Yet
another old picture of mine by Jorge
Cham, for I have contributed to the PHD Movie 2 on
While living in Madrid, I enjoyed its inimitable atmosphere and delicious food. For the latter, this Maribel's Dining Guide to Madrid (kindly provided by Aleks Nanevski) always came in handy.