Liens transverses ENS de Lyon

Agenda de l'ENS de Lyon

The Data-abstraction Framework: abstracting unbounded data-structures in Horn clauses, the case of arrays

mer 11 mai 2022



Soutenance de thèse d eM. BRAINE Julien sous la Direction de Mme GONNORD Laure

Langue(s) des interventions

Description générale

Proving properties on programs accessing data-structures such as arrays often requires universally quanti_ed invariants, e.g., \all elements below index i are nonzero". Instead of directly manipulating programs, we use Horn formulas which have recently become a popular format to express safety properties of programs.
In this PhD, we propose a general abstraction scheme operating on Horn formulas for unbounded data-structures. The main idea is to use abstraction to simplify the unbounded data-structures into simpler types such as integers. As such a simpli_cation loses information, not all safety properties can be proven after abstraction. It is thus key to choose the right abstraction for the given problem.
Our contribution is a general framework for which the data-structures and the abstraction to apply are parametrized. The speci_city of that framework is the attention spent to ensuring that our algorithm exactly implements the simpli_cation induced by the abstraction by using a property called relative completeness. This contrasts with previous work that mainly use benchmarks to prove the validity of the technique instead of analysing whether it veri_es a similar property.
Although the proposed framework is general and may theoretically handle data-structures such as trees, graphs, . . . , our focus has been on a speci_c abstraction of arrays that has already been studied in the literature called cell abstraction. This abstraction is of particular interest as it can handle most container algorithms.
The contribution of this PhD can be summarized into three parts. First, a demonstration that our framework in combination with cell-abstraction allows to express many existing techniques, and thus, our framework handles those as well. Secondly, a proof that a previous restricted technique actually satis_es relative completeness and an extension of it to handle a broader class of programs. Thirdly, the framework gives de_nitions, algorithms and theorems parametrized by the desired abstraction and, even though we have only used this framework for arrays, it gives the foundation for future abstraction of other data-structures.

Mots clés