Théo LOSEKOOT's PhD defense

General information

The defense will take place in room Métivier (Inria Rennes) at 9:00 on 17th December (UTC+1). It can be followed online at the following link (todo).
The current version of the thesis can be found here.

Jury Composition

Reviewers before defense

Naoki KOBAYASHI: Professor - The university of Tokyo
Mihaela SIGHIREANU Professeur des universités - ENS Paris-Saclay

Jury

Examiner : David BAELDE, Professeur des universités - ENS Rennes
Examiner : Naoki KOBAYASHI, Professor - The university of Tokyo
Examiner : Mihaela SIGHIREANU, Professeur des universités - ENS Paris-Saclay
Examiner : Jean-Marc TALBOT, Professeur des universités - Aix Marseille Université
PhD director : Thomas GENET, Professeur des universités - Université de Rennes
PhD co-director : Thomas JENSEN, Directeur de recherche - INRIA Rennes

Title and abstract

Title: Automatic Program Verification by Inference of Relational Models

Abstract: This thesis is concerned with automatically proving properties about the input-output relation of functional programs operating over algebraic data types. Recent results show how to approximate the image of a functional program using a regular tree language. Though expressive, those techniques cannot prove properties relating the input and the output of a function, e.g., proving that the output of a function reversing a list has the same length as the input list. In this thesis, we built upon those results and define a procedure to compute or over-approximate such a relation, therefore allowing to prove properties that require a more precise relational representation. Formally, the program verification problem reduces to satisfiability of Horn clauses on the theory of algebraic data types, which is here solved by exhibiting a Herbrand model of the clauses. In this thesis, we try to represent those Herbrand models not by regular tree languages but by relational formalisms, namely by convoluted tree automata and then by shallow Horn clauses, which generalize and simplify convoluted tree automata. The Herbrand model inference problem arising from relational verification is undecidable, so we propose an incomplete but sound inference procedure. Experiments show that this procedure performs well in practice w.r.t. state of the art tools, both for verifying properties and for finding counterexamples.



Updated in November 2024