About
I am a PhD candidate in LARA at EPFL, Switzerland, under the guidance of Prof. Viktor Kunčak. My research focuses on Formal Methods and Software Verification.
Before starting my PhD, I obtained an MSc in Computer Science from EPFL, Switzerland.
Beyond research
- Watchmaking — learning and practicing the craft in my free time
- Space exploration and astronomy
- All things aerospace and aviation
Research
My thesis, in one line: make software verification accessible.
Build verified software
A growing library of verified data structures, regex engines, and frameworks — proven correct, not just tested.
Build better tools
Improving verifiers like Stainless so that proving real-world code correct takes less expert effort.
Recent projects
Ziplex: Verified regex matching & linear-time invertible lexing
A linear-time invertible lexer verified in Stainless, built on top of a verified regex matcher using Brzozowski derivatives. The lexer follows longest-match semantics and is invertible with respect to printing. The project includes verified performance optimizations to achieve linear-time complexity including: a verified and reusable memoization framework based on my previous work on verified mutable hash tables; the memoization of critical functions using said framework; a zipper-based implementation for efficient regular expression derivative computation and memoization.
Verified ASN.1 serialization, with ESA
Verification of an ASN.1/ACN serialization protocol implementation, in collaboration with the European Space Agency. Published at VMCAI 2025.
Verifying the Scala standard library's LongMap
Full verification of a mutable, open-addressing hashtable from the Scala standard library. The proof uncovered a bug in the original implementation; my formally verified fix was accepted upstream. Published at IJCAR 2024.
Earlier projects
SVSHI — Secure and Verified Smart Home Infrastructure
My master thesis. SVSHI formally verifies Python smart building apps for KNX devices and manages KNX communications: a framework to develop and verify applications, plus a runtime system to run them on a KNX infrastructure.
Resource interfaces
An exploration of resource interfaces for programs — analogous to semantic interfaces, but expressing resource usage as a function of inputs — with a focus on serverless computing and a Python prototype extracting basic interfaces for simple programs.
Tools & code
I work on and with Stainless, the open-source program verifier for Scala developed at LARA, which uses SMT solvers to prove programs correct or find counterexamples.
Stainless on GitHubMuch of my verification work is open source in Bolts, a library of verified data structures, algorithms, and programs proven correct with Stainless.
Bolts on GitHubPublications
Talks
-
ZipLex: Formally Verified Linear-Time Invertible Lexer
-
Refinement Types in Scala with StainlessWith Katarzyna Marek and Matt Bovel
-
Mutable Cells for Memoized LexingVerified memoization framework for verified invertible lexing — invited talk
-
To Space and Back: Verified SerialisationFormally verifiable generated ASN.1/ACN encoders and decoders
-
Stainless Verifier and Composition in VerificationLMF Seminar on Software Verification
-
Verifying a Realistic Mutable Hash Table
Education
-
PhD in Computer Science
-
MSc & BSc in Computer Science
Resources
Interesting SMT queries
Interesting SMT queries I encountered in my projects. They can serve as benchmarks.
A slow cvc5 query
Generated by Stainless when verifying a "Bit Stream" implementation for the ASN.1 project. It takes a particularly long time to solve: ~100 s on my MacBook Pro, ~230 s on our Linux server. The smt2 file contains a comment header with options to pass to cvc5.