Apr 6 Our paper on mechanised verification of probabilistic properties of Bloom filters and their generalisations has been accepted to CAV 2020.


Dec 24 Our paper on enhancing deductive program synthesis with read-only permissions will appear at ESOP 2020.
Dec 23 My post on Composition in Distributed Systems has appeared in SIGPLAN PL Perspectives Blog.
Oct 24 Our work on Scilla has received a Distinguished Artifact Award at OOPSLA 2019.
Oct 8 I'm looking forward to give a keynote on the Scilla journey on October 11 at the 1st Workshop on Formal Methods for Blockchains in Porto. Here are the slides from my talk.
Sep 17 Delighted to be awarded a National Satellite of Excellence in Trustworthy Software Systems grant on the CertiChain project. An advert for postdoc positions will follow soon.
Sep 6 Our paper on Scilla, a smart contract language of Zilliqa blockchain will appear at OOPSLA 2019.
Sep 3 Our paper QED at Large: A Survey of Engineering of Formally Verified Software has been published in the journal on Foundations and Trends in Programming Languages. Download it from the publisher's site for free until 10 September 2019, or drop us a line if you need a copy.
Aug 12 I will be giving a talk entitled Functional Programming is Everywhere at Programming Languages Mentoring Workshop @ ICFP'19.
Aug 10 Kiran Gopinathan joins the team as a PhD student at SoC. Welcome, Kiran!
Aug 7 My post What Does It Mean for a Program Analysis to Be Sound? has appeared in SIGPLAN PL Perspectives Blog.
Jun 27 I will be giving a keynote talk at PODC 2019 on August 1.
May 30 ICFP Programming Contest 2019 will take place from 21 June 10:00am UTC till 24 June 10:00am UTC. It is free to participate, so don't miss this chance to flex your programming muscle and have some fun!
May 21 Bryan Tan joins as a summer intern at Zilliqa. Welcome, Bryan!
May 2 Amy Zhu joins the team as an intern. Welcome, Amy!
May 1 Our paper on Exploiting The Laws of Order in Smart Contracts with Aashish Kolluri, Ivica Nikolić, Prateek Saxena, and Aquinas Hobor got accepted to ISSTA 2019.
Apr 17 I have been awarded the AITO Dahl-Nygaard Junior Prize, and will be giving an associated keynote at ECOOP'19 in July. Here's the related News Entry at NUS School of Computing page.
Mar 26 Will be serving on the programme committee for CPP 2020, a conference where you should submit your next masterpiece, formally verified in Coq (or any other proof assistant).
Mar 6 Yunjeong Lee joins the team as an intern. Welcome, Yunjeong!
Jan 31 Our POPL'19 paper on program synthesis, made it to NUS School of Computing news and to Yale-NUS College news.
Jan 9 I will be giving a talk on How to Bootsrap a Research Project at Programming Languages Mentoring Workshop @ POPL'19.


Nov 28 A work-in-progress report on probabilistic verification of security properties of blockchain protocols will be presented by Kiran Gopinathan at CoqPL 2019.
Nov 12 Gave a talk entitled What We Talk about When We Talk about Formally Verified Systems at Blockchain and Cybersecurity Workshop 2018 hosted by National University of Singapore.
Nov 5 A paper on practical programming with distributed protocos (with Kristoffer Just Andersen), will appear at PADL 2019.
Oct 9 Two papers accepted at POPL 2019: on program synthesis via Separation Logic (with Nadia Polikarpova), and on proving no-false-positives for unsound static race detectors (with Nikos Gorogiannis and Peter O'Hearn).
Sep 8 Looking forward to visit Dominique Devriese at KU Leuven on September 19 and give a talk on program synthesis with Separation Logic.
Aug 29 On September 3-5, I will be visiting Éric Tanter and the research group of Cătălin Hriţcu at INRIA Paris.
Aug 23 Our paper on Finding the Greedy, Prodigal, and Suicidal Contracts at Scale with Ivica Nikolić, Aashish Kolluri, Prateek Saxena and Aquinas Hobor got accepted to ACSAC 2018.
Aug 15 I am looking forward to visit Sukyoung Ryu and Hongseok Yang and their groups at KAIST in Daejeon on August 23-28.
Aug 14 On August 21, I will be giving a series of lectures on implementation and verification of distributed systems and their applications at SIGPL Summer School 2018 in Seoul (yes, that page is entirely in Korean, but, even if you are, just like me, not a Korean speaker, you can still try to identify the titles of my talks there).
Aug 6 Scilla, a strongly typed intermediate language for smart contracts developed by Zilliqa, is now open-sourced: here's the repository, and here's a new shiny web page with tutorials and documentation. Contributions are welcome!
Jul 20 Got promoted to an Associate Professor of Computer Science at UCL, effective 1st October 2018.
Jul 6 Our paper on RacerD, an industrial-scale compositional static race detector, developed at Facebook, with Sam Blackshear, Nikos Gorogiannis, and Peter O'Hearn, is conditionally accepted at OOPSLA 2018. Here's the preprint.
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 7 I will be leaving UCL in October 2018, and will move to Singapore, joining Yale-NUS College as an Assistant Professor.
Jun 6 Amrit Kumar 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 ECOOP 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.
Feb 7 I will be serving on the programme committee of APLAS 2018. The symposium is going to take place on the 3rd–7th December in Middle-earth New Zealand, so make sure to submit your awesome works to go there!
Jan 16 Kristoffer Just Andersen from Aarhus University joins the group as a visiting PhD researcher for five months to work on program logics for composable distributed systems.
Jan 3 Our joint position paper with Amrit Kumar and Aquinas Hobor on Scilla, a new verification-friendly intermediate-level language for smart contracts, is now available.


Dec 21 Our paper on a modular specification and a refinement-based proof of Multi-Paxos consensus protocol (joint work with Álvaro García Pérez, Alexey Gotsman and Yuri Meshman) is accepted to appear at ESOP 2018. The accompanying proof-of-concept prototype is available here.
Dec 11 Once again, I'm organising a Scenario Week Competition on Computational Geometry problems, as a part of UCL course on Systems Engineering. UPD: The concluding slides with the statistics are here.
Nov 15 Our paper on a Mechanised Blockchain Consensus (joint work with George Pîrlea) is accepted to appear at CPP 2018. The accompanying Coq development is available here.
Nov 7 I am excited to welcome Maria A Schett and Thomas Sibut-Pinote, who have joined the group to work on program logics and semantics for reasoning about distributed systems and smart contracts.
Nov 6 Programs and Proofs are updated for Coq 8.7.
Sep 26 Our paper on a Separation Logic for verification of distributed systems, with James R. Wilcox and Zachary Tatlock, is accepted to appear at POPL 2018.
Sep 12 I will be serving on the programme committee of ICFP 2018.
Aug 10 Awarded an eight-month grant by Research Institute in Verified Trustworthy Software Systems for the project Automated Reasoning with Fine-Grained Concurrent Collections, in collaboration with Nikos Gorogiannis.
Jul 20 I'm co-chairing (together with Yves Bertot) the CoqPL 2018 workshop, co-located with POPL 2018 in Los Angeles, CA in January. Details and submission guidelines here.
May 18 I'm chairing the ICFP 2017 Student Research Competition. A good poster presentation is a great chance to show off your (or your PhD students') research, and it will drastically improve your chances to get valuable feedback before submitting a POPL paper. There are also money prizes, so go ahead and submit an extended abstract! Deadline is July 10.
Apr 24 Invited to serve on the PC of 15th Asian Symposium on Programming Languages and Systems (APLAS 2017) and Scala Symposium 2017.
Apr 12Paper on verified concurrent data structures with changeable-post-factum histories is accepted to ECOOP 2017.
Mar 24I'm giving an invited talk at Programming Languages and Compilers conference in Rostov-on-Don on 3-5 April 2017.
Mar 6The registration for the 6th South of England Regional Programming Language Seminar (S-REPLS 6), which will take place at UCL on May 25, is now open. Please, indicate your attendance by participating in this poll.
Mar 5 Our position paper on type theory for compositionally verified distributed systems will appear at SNAPL 2017.
Feb 20 I'm organising a Scenario Week Competition on Computational Geometry problems, as a part of UCL course on Software Engineering. The concluding slides from the competition are here.


Dec 15 An extended version of our POPL'14 paper on cardinality analysis featuring new cool evaluation of the analysis (im)precision has been accepted for publication in Journal of Functional Programming.
Nov 15 Announced a postdoc poisition on compositionally verified distributed systems. Details above.
Oct 3 Awarded with EPSRC First Grant on Program Logics for Distributed Systems.
Sep 25 Invited to serve on the PC of Static Analysis Symposium 2017.
Nov 1 I'm serving on the PC of the 1st Workshop on Trusted Smart Contracts. Submit your ideas on programmable cryptocurrencies!
Aug 27 Paper on specifying and verifying non-linearizable concurrent objects is accepted to OOPSLA 2016.
Jun 10 The slide with the flow of ideas in modern concurrency logics is now available here.
Jun 5 I'm serving on the PC of Scala Symposium 2016. Submit papers on your Scala projects!
May 25 Paper on QuickChecking computational geometry algorithms is accepted to ICFP 2016.
Mar 15 I will be serving on the programme committee of TAPAS 2016. Submit proposals for your talks on static analysis!
Feb 17 "Programs and Proofs" are now updated for Coq 8.5 and Ssreflect 1.6.
Feb 1 I'm organizing Scenario Week on Computational Geometry as a part of Software Engineering and HCI course at UCL.
Jan 15 I will be serving on the programme committee of POPL 2017.
Jan 10 PPLV@UCL has an opening for a lecturer position.


Dec 30 New blog post on Lamport's critique of compositionality.
Dec 12 I will be teaching the Theory II module in Spring 2016.

Main page