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 languages, software verification, distributed systems, and program synthesis. 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
|Office Phone:||+65 6601 1466|
- 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 (please, check the lab page for the relevant topics first) and apply here. The application deadlines are 15 June and 15 December.
- Research internships: In case if you are interested in an internship, please send me an email with your CV and a paragraph of text describing your specific interests in the topics of my reseatch (see the lab page for more details). Strong background in PL/logic/verification or systems-building is a must. I welcome candidates who will commit six months or longer to focused research on-site, and generally unable to respond to requests otherwise.
|Aug 23, 2023||Our paper on designing and implementing Extract Method refactoring for Rust (joint work with Sewen Thy, Andreea Costea, and Kiran Gopinathan) will appear at OOPSLA’23.|
|Aug 11, 2023||Our work on fuzzing distributed systems has been accepted at CCS’23.|
|May 26, 2023||Two awards at the upcoming PLDI’23:|
|Apr 7, 2023||
Two papers accepted at PLDI’23:
|Mar 17, 2023||I’ve had great time visiting CISPA (hosted by Swen Jacobs), where I gave a talk on the current state of the SuSLik synthesiser.|
|Mar 12, 2023||I have participated in the Dagstuhl Seminar on Unifying Formal Methods for Trustworthy Distributed Systems, which we have co-organised with Roopsha Samanta, Swen Jacobs, and Ken McMillan. It was fun.|
|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.|
- Greybox Fuzzing of Distributed Systems30th ACM Conference on Computer and Communications Security (CCS) 2023. ACM.
- Mostly Automated Proof Repair for Verified LibrariesProc. ACM Program. Lang. 2023. Vol. 7, (PLDI), Pages 107:1–107:25. ACM.ACM SIGPLAN Distinguished Paper Award
- Leveraging Rust Types for Program SynthesisProc. ACM Program. Lang. 2023. Vol. 7, (PLDI), Pages 164:1–164:24. ACM.Distinguished Artifact Award
- Cyclic Program SynthesisPLDI 2021. Pages 944–959. ACM.ACM SIGPLAN Distinguished Paper Award
- Practical Smart Contract Sharding with Ownership and Commutativity AnalysisPLDI 2021. Pages 1327–1341. ACM.
- Safer Smart Contract Programming with ScillaProc. ACM Program. Lang. 2019. Vol. 3, (OOPSLA), Pages 185:1–185:30. ACM.Distinguished Artifact Award
- Structuring the Synthesis of Heap-Manipulating ProgramsProc. ACM Program. Lang. 2019. Vol. 3 (POPL), Pages 72:1–72:30. ACM.ACM SIGPLAN Distinguished Paper Award
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.