Automatic Program Verification by Inference of Relational Models

The defense will take place in room Métivier (Inria Rennes/IRISA) at 9:00 on 17th December (UTC+1).

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.