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. I learn and practice this craft during my leisure time.

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 to contracts or prove their validity.

My main goal with my thesis is to make software verification more accessible. I plan to contribute in that direction through two axes: first, by developing a library of verified software or verified frameworks (e.g., data structures, a regular expression matching engine, a lexing framework), and second, by contributing to tool development to make verifying software easier and, therefore, more widespread.

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.
• ()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

[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

(slides) Verifying a Realistic Mutable Hash Table. IJCAR 2024.

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.