Research
Plan de la page

See the list of all my publications

PhD

The goal of my thesis is to develop static analysis methods that enable the verification of strong properties, such as partial functional correctness, for components of operating systems that manipulate inductive data structures.

See (Giet et al., 2023) for the abstract representation of memory states.

Internships

Detecting race conditions in the Linux Kernel using memory barriers

The Linux Kernel uses pairs of memory barriers to avoid race conditions. When a novel element is added then a value \(A\) is set before a second one \(B\). And the code uses a memory barrier to ensure that \(B\) is not assigned before \(A\). When the value \(A\) must be read, the program first checks whether \(B\) was correctly set. And a second memory barrier separates the two reads. These barriers ensure that neither the compiler nor the CPU could reorder these read/write operations.

During a 6-month internship, I worked with Baptiste Lepers at the university of Sydney on the detection of race conditions in the Linux kernel using incorrectly matched memory barriers.

See (Lepers et al., 2023) for more details.

Precise analysis of finite state machine in the Astrée analyzer

Critical systems, like those used in cars or aircraft, utilize finite state machines to model control and command functions. These systems are also required to be proven free of “crashs” (formally, undefined behavior). To do so, abstract interpretation based static analyses over approximates the state of the program at any point. In the case of automaton, the control flow is not explicitly visible in the code. It depends on the states transition, that is to say the assignment of some variables.

During a 5-month internship at AbsInt, I extended the Astrée analyzer to take into account finite state machines. This extension is capable to detect and precisely analyse generated implementation of finite state machine by using dynamic partitioning.

See (Giet et al., 2019) for more details.

Decision procedures for modal logic

During a 2-month internship at ISAE-Supaéro under the direction of Christophe Garion and Rémi Delmas, I implemented a generic satisfiability solver for the K-Modal logic. I later extended it to prove satisfiability of a family of epistemic logics.

See (Delmas et al., 2018) for more details (article in french).

Bibliography

Delmas, R., Garion, C., Giet, J., 2018. MOLOSS, un solveur pour la satisfiabilité en logique modale, in: Journées Nationales de l’intelligence Artificielle Fondamentale (JIAF’18).
Giet, J., Mauborgne, L., Kästner, D., Ferdinand, C., 2019. Towards zero alarms in sound static analysis of finite state machines, in: Romanovsky, A.B., Troubitsyna, E., Bitsch, F. (Eds.), Computer Safety, Reliability, and Security - 38th International Conference, SAFECOMP 2019, Turku, Finland, September 11-13, 2019, Proceedings, Lecture Notes in Computer Science. Springer, pp. 3–18. https://doi.org/10.1007/978-3-030-26601-1\_1
Giet, J., Ridoux, F., Rival, X., 2023. A product of shape and sequence abstractions, in: Hermenegildo, M.V., Morales, J.F. (Eds.), Static Analysis. Springer Nature Switzerland, Cham, pp. 310–342.
Lepers, B., Giet, J., Lawall, J., Zwaenepoel, W., 2023. OFence: Pairing Barriers to Find Concurrency Bugs in the Linux Kernel, in: EuroSys 2023 : Eighteenth European Conference on Computer Systems. ACM, Rome, Italy, pp. 33–45.