I do research in programming language design and implementation, software verification, 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.
Yale-NUS College, 28 College Avenue West
#01-501, Singapore 138533
||RC3-01-03E, Cendana (Yale-NUS), COM2-02-42 (NUS SoC)|
|Office Phone:||+65 6516 1903|
|Office Hours:||by request (Summer 2021)|
|Availability:||Outlook Calendar (takes a while to load)|
I run the NUS PLSE Seminar Series. Get in touch if you want to particiapte!
|May 27, 2021||Got tenure!|
|May 24, 2021||Our paper on Cyclic Program Synthesis has received PLDI 2021 Distinguished Paper Award!|
|Apr 20, 2021||Looking forward to serve on the programme committees of International Symposium on DIStributed Computing (DISC’21) and of the 3rd International Workshop on Formal Methods for Blockchains (FMBC’21). Make sure to submit your papers on (verified) distributed systems, blockchains, and their applications for quality feedback (and, hopefully, publication)!|
|Apr 12, 2021||Our PLDI’21 paper on smart contract sharding with static analysis is now available.|
|Feb 26, 2021||
Two papers (conditionally) accepted at PLDI’21:
|Dec 11, 2020||I will serve as a Programme Committee Chair for ESOP’22.|
|Dec 1, 2020||Yutaka Nagashima joins the team as a postdoc. Welcome, Yutaka!|
|Nov 30, 2020||Our paper on Automated Repair of Heap-Manipulating Programs from Separation Logic-style specifications will appear at VMCAI 2021.|
- Cyclic Program SynthesisPLDI 2021. ACM.PLDI 2021 Distinguished Paper Award
- Practical Smart Contract Sharding with Ownership and Commutativity AnalysisPLDI 2021. 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.
I am married to CG artist Lilia Anisimova.
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.