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.

Outside of my academic pursuits, I am a passionate watchmaking enthusiast, learning and practicing this craft during my leisure time. I am also passionate about space exploration, astronomy, and everything aerospace and aviation related.

Research

My current research focuses on software verification, particularly with Stainless, a verifier for a subset of Scala that uses SMT solvers to find counterexamples or prove validity.

My main goal with my thesis is to make software verification more accessible by:

  • Developing a library of verified software or frameworks (e.g., data structures, a regex engine, etc.)
  • Contributing to tool development to simplify software verification

My recent projects include:

  • Verifying the LongMap of the Scala standard library, a mutable hashtable based on open addressing. This work has been published at IJCAR24. This verification work led to the discovery of a bug in the standard library implementation. I proposed a fix that I fully formally verified, which has been accepted.
  • Implementing and verifying an implementation of Regex matching with derivatives. I then use this Regex engine to implement a lexer (or tokeniser) that is verified to be correct and invertible under certain conditions.
  • Verifying the correctness of the implementation of a serialization protocol, ESN1, in collaboration with the European Space Agency. This work will be published at VMCAI25.

Part of my verification work is available on Bolts, a library of programs verified with Stainless.

Some of my past projects include:

  • (Master thesis) SVSHI: Secure and Verified Smart Home Infrastructure. SVSHI formally verifies Python smart building apps for KNX devices and manages KNX communications. Specifically, SVSHI consists of a framework to develop and verify Python applications and a runtime system to manage a KNX infrastructure with these applications. The code is available on GitHub here.
  • (Report) Resource interfaces: I explored the idea of resource interfaces for programs. The concept is analog to semantic interfaces that are widely used, but to express the resource usage of a program given its inputs instead of its behaviour. I particularly explore the application of such resource interfaces to serverless computing. I also built a prototype in Python to extract basic interfaces for simple programs. The experience gave me a better understanding of serverless computing and its applications, as well as some practical experience with commercial solutions like Amazon Lambda.

Publications

  • [5] Bucev, M., Chassot, S., Felix, S., Schramka, F., Kunčak, V. (2025). Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study In Verification, Model Checking, and Abstract Interpretation (pp. 185-207). Springer Nature Switzerland.
  • [4] (pdf) Chassot, S., Kunčak, V. (2024). Verifying a Realistic Mutable Hash Table. In: Benzmüller, C., Heule, M.J., Schmidt, R.A. (eds) Automated Reasoning. IJCAR 2024. Lecture Notes in Computer Science(), vol 14739. Springer
  • [3] (pdf) (Preprint) (Master Thesis) Andrea Veneziano, and Samuel Chassot. "SVSHI: Secure and Verified Smart Home Infrastructure." (2022).
  • [2] (pdf) (Preprint) Samuel Chassot. "Development of a NIC driver in C#" .CoRR abs/2107.12833 (2021).
  • [1] (pdf) Daniel Filipe Nunes Silva, Samuel Chassot, Luca Barras, Deblina Bhattacharjee, and Sabine Süsstrunk. "Scaling up an Unsupervised Image-to-Image Translation Framework from Basic to Complex Scenes". American Journal of Computer Science and Technology 4, no.4 (2021): 97-105.

Talks

  • To Space and Back: Verified Serialisation (Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study), (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

This section contains interesting SMT queries I encountered in my projects. They can serve as benchmark.

  • [cvc5 slow query] This query is generated by Stainless when verifying a "Bit Stream" implementation for the ASN.1 project mentio§ned above. It is interesting because it takes a particulary long time to solve: ~100 sec on my Macbook Pro, ~230 sec on our linux server. The smt2 file contains a comment header with options to pass to cvc5.