News
2025
- Our paper ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis has been accepted at the Dafny workshop at POPL 2026.
17 Nov 2025
- Our paper MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification has been accepted at the Dafny workshop at POPL 2026.
17 Nov 2025
- Our paper DafnyPro: LLM-Assisted Automated Verification for Dafny Programs has been accepted at the Dafny workshop at POPL 2026.
17 Nov 2025
- Our paper CLEVER: A Curated Benchmark for Formally Verified Code Generation has been accepted at NeurIPS 2025.
20 Sep 2025
- I'm organizing the latest edition of the South of England Regional Programming Languages Seminar (SREPLS) at Amazon UK's headquarter in London on 29th October 2025.
20 Sep 2025
- Our paper CLEVER: A Curated Benchmark for Formally Verified Code Generation has been accepted at the AI for Math Workshop at ICML 2025.
10 Jul 2025
- Our paper Verified Foundations for Differential Privacy won a Distinguished Artifact Award at the 46th Conference on Programming Language Design and Implementation (PLDI 2025)!
9 Jul 2025
- The preprint of the paper CLEVER: A Curated Benchmark for Formally Verified Code Generation is now available on arXiv.
28 May 2025
- The paper Verified Foundations for Differential Privacy has been accepted at the 46th Conference on Programming Language Design and Implementation (PLDI 2025).
18 Mar 2025
- I am serving on the program committee of the 37th International Conference on Computer-Aided Verification (CAV).
14 Feb 2025
- I gave a talk on the paper Verifying the Fisher-Yates Shuffle Algorithm in Dafny at the Dafny workshop at POPL 25.
19 Jan 2025
- The paper Verifying the Fisher-Yates Shuffle Algorithm in Dafny is now accessible on arXiv.
10 Jan 2025
- The paper Dafny as Verification-Aware Intermediate Language for Code Generation is now accessible on arXiv.
10 Jan 2025
2024
- The paper Compiler Fuzzing in Continuous Integration: a Case Study on Dafny has been accepted at the 18th International Conference on Software Testing, Verification and Validation (ICST).
10 Dec 2024
- The preprint of the paper Verified Foundations for Differential Privacy is now accessible on arXiv.
3 Dec 2024
- I gave a talk at the 21st International Colloquium on Theoretical Aspects of Computing (ICTAC).
27 Nov 2024
- The paper Verifying the Fisher-Yates Shuffle Algorithm in Dafny has been accepted at the Dafny workshop at POPL 25.
21 Nov 2024
- The paper Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny has been accepted at the Dafny workshop at POPL 25.
21 Nov 2024
- The paper Dafny as Verification-Aware Intermediate Language for Code Generation has been accepted at the Dafny workshop at POPL 25.
21 Nov 2024
- The paper Randomised Testing of the Dafny Compiler: Into the CI has been accepted at the Dafny workshop at POPL 25.
21 Nov 2024
- I am serving as an artifact evaluator at the Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH).
21 Nov 2024
- I attended the Formal Specification and Validation at Scale workshop of the Research Institute on Verified Trustworthy Software Systems (VeTSS) at the Isaac Newton Institute.
22 Oct 2024
- I am serving as an artifact evaluator at the 52nd Symposium on Principles of Programming Languages (POPL 2025).
1 Oct 2024
- The paper Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny with Wojciech Różowski has been accepted at the 21st International Colloquium on Theoretical Aspects of Computing (ICTAC).
2 Sep 2024
- The Dafny workshop is returning to POPL in 2025! Please consider submitting.
21 Aug 2024
- I had a great time mentoring Yue Chen Li during his now completed internship in Amazon Web Services' Automated Reasoning Group.
21 Aug 2024
- I attended the Annual Meeting of the Research Institute on Verified Trustworthy Software Systems (VeTSS) at the Royal Academy of Engineering.
21 May 2024
- I gave a talk on Dafny at the Fourteenth South of England Regional Programming Languages Seminar (S-REPLS 14) at Jane Street.
8 Mar 2024
- I published a post in the Dafny Blog.
12 Jan 2024
2023
- The paper VMC: a Dafny Library for Verified Monte Carlo Algorithms has been accepted at the Dafny workshop at POPL 24.
15 Nov 2023
- I published a post in the Dafny Blog.
8 Nov 2023
- I gave a talk on Dafny at the University of Birmingham.
3 Nov 2023
- I gave talks on Dafny at Cornell and Oxford University.
16 Oct 2023
- I gave a talk on Dafny in the LLAMA seminar series at the ILLC of the University of Amsterdam.
4 Oct 2023
- I am organizing a workshop on Dafny that will be co-located with POPL 2024 in London.
29 Sep 2023
- My PhD thesis Canonical Algebraic Generators in Automata Learning is now available online.
8 Aug 2023
- I am attending the 35th International Conference on Computer Aided Verification (CAV) in Paris.
17 Jul 2023
- I gave a talk on Dafny in the Programming Principles, Logic, and Verification Seminar at University College London (UCL).
29 Jun 2023
- I gave a talk at the 10th Conference on Algebra and Coalgebra in Computer Science (CALCO).
21 Jun 2023
- The paper Generators and Bases for Monadic Closures has been accepted at the 10th Conference on Algebra and Coalgebra in Computer Science (CALCO).
29 Apr 2023
- I successfully defended my PhD thesis Canonical Algebraic Generators in Automata Learning at University College London.
27 Apr 2023
- I volunteered as subreviewer for the 10th Conference on Algebra and Coalgebra in Computer Science (CALCO).
18 Apr 2023
- I volunteered as subreviewer for the 29th International Symposium on Model Checking of Software (SPIN).
1 Mar 2023
- I have been accepted as a member of the Artifact Evaluation Committee of the 35th International Conference on Computer Aided Verification (CAV).
19 Jan 2023
- I have submitted my PhD thesis Canonical Algebraic Generators in Automata Learning at the Univerity College London.
15 Jan 2023
2022
- I started as full-time Applied Scientist in the Dafny programming language team within the Automated Reasoning Group of Amazon Web Services.
21 Dec 2022
- I completed my Software Engineering internship in the Hack programming language team of Meta.
27 Sep 2022
- I gave a presentation at the 38th International Conference on Mathematical Foundations of Programming Semantics (MFPS 22) at Cornell University.
12 July 2022
- I gave a presentation at the Programming Principles, Logic, and Verification Seminar of the University College London.
28 June 2022
- The paper Guarded Kleene Algebra with Tests: Automata Learning has been accepted at the 38th International Conference on Mathematical Foundations of Programming Semantics (MFPS 22).
10 June 2022
- I have accepted an internship offer from Meta. I will be working on the (type system of the) Hack programming language.
02 Mar 2022
- I gave a presentation at the Lectures on Logic and its Mathematical Aspects Seminar series at the Institute for Logic, Language & Computation (ILLC) of the University of Amsterdam.
26 Jan 2022
2021
- The paper Canonical Automata via Distributive Law Homomorphisms has been accepted for presentation at the 8th Symposium on Compositional Structures (SYCO 8).
10 Nov 2021
- I am currently interning as Applied Scientist in the Automated Reasoning Group of Amazon Web Services (AWS) under the supervision of Rustan Leino.
3 Sep 2021
- The paper Canonical Automata via Distributive Law Homomorphisms has been accepted for publication at the 37th Conference on the Mathematical Foundations of Programming Semantics (MFPS 21).
3 Sep 2021
- I am serving as a student volunteer at the International Conference on Computer-Aided Verification (CAV) and the International Colloquium on Automata, Languages and Programming (ICALP).
25 May 2021
- The preprint of the paper Canonical Automata via Distributive Law Homomorphisms can be found on arXiv.
29 Apr 2021
- I am serving as a mentor at the Symposium on Principles of Programming Languages (POPL).
16 Jan 2021
2020
- I am serving as a student volunteer and mentor at the Conference on Systems, Programming, Languages, and Applications (SPLASH).
31 Oct 2020
- I am a teaching assistant for Logic and Database Theory, Discrete Mathematics for Computer Scientists, and Computability and Complexity.
21 Oct 2020
- You can now find a preprint of the paper Bases for Algebras Over a Monad on arXiv.
20 Oct 2020
