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 recent projects include:
- Verifying the LongMap of the Scala standard library, a mutable hashtable based on open
addressing. This
work will be published at IJCAR24.
- 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.
- Verifying the correctness of the implementation of a serialization protocol, ESN1, in
collaboration with
the European Space Agency.
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.
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.