This thesis studies how regular tree languages can be used to automatically verify properties on higher-order functional programs. Our goal is to develop new techniques and tools for the programmers to develop safer programs while reducing the time and expertise needed to verify them.
In particular, we focus on the automatic verification of regular safety properties, a family of properties for which we show that completely and fully automatic verification can be achieved.
Our verification method is build upon a regular abstraction procedure that can automatically learn regular tree languages that over-approximates of the reachable states of a program, allowing the verification of a target property.
By using regular languages as types we modularize this procedure to verify complex properties
by stating them as type inference problems.
In addition we study the performances of the overall technique in our prototype OCaml implementation in the Timbuk 4 verification framework over a test suite of more than 80 verification problems.
We then show how our abstraction procedure can be used to verify relational properties that seemed out of the scope of regular tree languages.
To do that, we use and extend a convolution operator on trees to represent every element of a relation into a regular tree language. We can then extend our previously defied regular language learning
procedure to automatically infer such regular relations.
We propose a Rust implementation of this idea as a regular solver for Constrained Horn Clauses systems and study its performance on several relational verification problems.
Lien de connexion pour suivre la soutenance :
https://bbb.irisa.fr/b/gen-hmm-jjk
Naoki Kobayashi, Professeur Université de Tokyo.
Mihaela Sighireanu, Professeur ENS Paris-Saclay.
Jasmin Blanchette, Professeur Vrije Universiteit Amsterdam.
Sophie Pinchinat, Professeur Univ Rennes.
Thomas Genet, Maître de conférences Univ Rennes (co-dir).
Thomas Jensen, Directeur de recherche Inria (co-dir).