Samuel Chassot

About

My name is Samuel Chassot. 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

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 GitHub

Much of my verification work is open source in Bolts, a library of verified data structures, algorithms, and programs proven correct with Stainless.

Bolts on GitHub

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

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.

Paper

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 resuable 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 expressionderivative computation and memoization.

Paper

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.

Paper

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.

GitHub

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.

Report

Publications

Talks

Refinement Types in Scala with Stainless

With Katarzyna Marek and Matt Bovel — Scala Workshop 2026

Details Slides
Mutable Cells for Memoized Lexing

Verified memoization framework for verified invertible lexing — invited talk, VIMPL 2026

Slides
To Space and Back: Verified Serialisation

Formally verifiable generated ASN.1/ACN encoders and decoders — VMCAI 2025

Slides
Stainless Verifier and Composition in Verification

LMF Seminar on Software Verification, 2024

Slides
Verifying a Realistic Mutable Hash Table

IJCAR 2024

Slides

Miscellaneous 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.

smt2 file