Department of Computer Science
University College London
Gower Street, London WC1E 6BT
||Room 5.02, Malet Place Engineering Building|
|Office Phone:||+44 20 7679 0319 (Internal: 30319)|
|Calendar:||Outlook.com (it takes a while to load)|
|Office hours:||Thursday, 14:00-15:00 (please, email me first).|
I do research in programming language theory, including, but not limited to types, semantics, and software verification. Lately, I have been mostly focusing on developing sound and scalable methodologies for building provably correct concurrent and distributed systems (with applications to blockchains and smart contracts). For my work, I write a lot of mechanised proofs in Coq, as well as functional code in Scala, OCaml, and Haskell.
Since November 2015, I am a member of the Programming Principles, Logic and Verification group at the Department of Computer Science of University College London. Prior to joining UCL, from December 2012 to October 2015, I was a postdoc at IMDEA Software Institute. From November 2008 to November 2012, I was a research assistant in the CS Department of KU Leuven, where I obtained my PhD. During my doctoral studies I was a visiting PhD fellow in the Department of Computer Science of Aarhus University and a research intern in the PPT group at MSR Cambridge. I got my MSc degree in Mathematics and CS in 2008 from Dept. of Mathematics and Mechanics of Saint Petersburg State University. Before joining academia I worked as a software developer at JetBrains.
If you are looking for the "CSL Family Tree" slide, you can find it here. Other slides from my recent talks are here.
Curriculum Vitae: [PDF]
|Jun 20||Kiran Gopinathan and Oscar King join the group as research interns for Summer 2018. They will be working on implementation and verification of blockchain protocols.|
|Jun 6||Amrit and I gave a long interview to Epicenter about Scilla and formal verification of smart contracts.|
|Jun 1||Next year, I will be serving on the Programme Committees of PLDI 2019 and OOPSLA 2019. Looking forward for reading lots of (your) exciting submissions on types, logics, compilers, verification, and program synthesis!|
|Mar 21||I am thrilled to be amongst the recipients of the Google Faculty Research Award 2017 and looking forward to advance the state of the art in verified optimisations for distributed systems. Here is the full list of this year recipients.|
|Mar 7||I am really excited to join the amazing Zilliqa team as an advisor on formal methods to collaborate on safe and secure programming languages for smart contracts.|
|Mar 1||I've made an appearance in another article on smart contracts, this time by MIT Technology Review. Not sure I fully agree with its tone, though.|
|Feb 22||Our technical report on a symbolic analysis of Ethereum smart contracts for trace vulnerabilities got featured in an article by Vice's Motheboard. Amongst other things, our paper gives hints on how to become $6,000,000 richer, so you might want to read it.|
|Feb 15||I will be on the programme committee of POPL 2019. I should probably encourage you to submit your cutting edge PL research there, but I know you will do it anyway.|
I am a also a creator of the La Clojure plugin for IntelliJ IDEA. It is no longer maintained, but its sources are available on GitHub.
Check my GitHub profile for my other projects.
Over the years, I have been very lucky to work on joint research projects with some great people:
I am married to CG artist Lilia Anisimova.
I am on Twitter as @ilyasergey.
My Erdős number can be found here (last time I checked it was 4).
The photo above is couresy of Elena Alhimovich. Here is my "official" photo,
suitable for appropriate occasions. Yet another 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.