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
- [6] Milovančević, D., Bucev, M., Wojnarowski, M., Chassot, S., Kunčak, V. (2025). Formal Autograding in a Classroom. In: Vafeiadis, V. (eds) Programming Languages and Systems. ESOP 2025. Lecture Notes in Computer Science, vol 15695. Springer, Cham.
- [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 mentioned 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.
