Guilhem Ardouin

An overview of my past and ongoing projects.

INTERNSHIP 2025 (ongoing): Confidence-based safety properties in CAISAR

CAISAR public repository: gitlab

With the increasing use of machine learning (ML) in our daily life systems comes the need to certify that these systems are working properly. However, certifying that a ML model is completely safe is yet not feasible, but it is possible to specify and verify some properties to obtain formal guarantees on the behavior of a model. Currently, the properties that are effectively provable are local robustness and some variants. This is only a narrow set of properties, and it could be interesting to be able to verify more general properties such as global robustness and global fairness.

To this aim, the notion of confidence-based safety property have been recently introduced by Athavale et al., where the safety of a neural network is examined by additionally considering the confidence of the model on its predictions. Yet, only a proof of concept implemented in Marabou, a tool for verifying neural networks, exists, making this approach difficult to apply on a wider scale. Indeed, one would want to specify and prove such properties in other provers, for instance PyRAT or Beta-CROWN.

The goal of my internship is to be able to write an efficient formal specification of confidence-based safety properties in CAISAR, an open source platform for the specification and verification of machine learning models which unifies the interface for several AI verification tools. Such feature would represent a generalization of the concept of confidence-based safety properties by making it available for a wide range of provers that are supported by CAISAR.

INTERNSHIP 2024: Symbolic execution directed by A*

Project repository: github
Documentation: pdf
User manual: pdf

Symbolic execution is an inefficient approach for large programs: this is a consequence of the explosion in the number of paths in the execution tree, and even the potential infinity of the symbolic execution tree. It is nevertheless possible to consider new heuristics to improve this approach. Work carried out by my supervisors addresses this problem and has led to two new search strategies inspired by the A* algorithm. These heuristics have been implemented in BINSEC, a tool that uses symbolic execution for binary programs. However, these approaches can also be implemented in other tools, such as KLEE, which enables symbolic execution on programs written in higher-level languages. The aim of my internship was therefore to implement these search heuristics in KLEE, as well as all the functionality required to perform reachability analysis with this program.

My work therefore led to the design of an extension to KLEE enabling these new heuristics to be used. In particular, I had to think about the problem of making KLEE capable of carrying out reachability analysis, as the tool was not initially designed for this. I was then able to draw inspiration from the way existing heuristics work in KLEE in order to implement the new A* heuristics. The implementation of these heuristics also required the addition of features such as the collection of certain information during symbolic execution. Finally, as the A* heuristics take into account the distance between an instruction and the target to be reached, I also designed an external tool, developed in Python, to calculate these distances and use them in the new exploration strategies.

INTERNSHIP 2023: Development of a Visual Studio Code extension for TChecker

Project repository: github
Documentation: pdf

TChecker is a model-checking verification tool for real-time systems, developed at the LaBRI by Frédéric Herbreteau and Gérald Point. It is also used by several researchers, notably in France and India, to develop and test their own verification algorithms. TChecker is made up of a number of tools for validating models syntactically, simulating them and verifying them formally.

In order to facilitate the use of the various TChecker tools, I have developed an extension for Visual Studio Code, which mainly allows:

• syntax highlighting of models
• editing assistance (auto-completion, signature display, hover)
• use of TChecker tools in the VSCode environment