< Retour au sommaire

Soutenance de thèse de Hichem Rami Ait El Hara

Titre: Theory of sequences tailored for program verification

le

Lieu: Amphi 34

Suivre en visio

Abstract

The choices of semantic models for a programming language have a significant effect on the efficiency of the verification of programs in that language. Indeed, many verification techniques generate mathematical formulas using those models. The mathematical theories used in these formulas and their shape have a direct impact on their solvability by the used solver. The modelization of memory and data structures often uses the SMT (Satisfiablity Modulo Theories) theory of arrays which is well established and used in SMT solvers. In this theory, arrays associate values with indices, both of which can be of any type. The theory also allows for operations that enable the writing and reading of the stored data. However, in the concrete programs from which the formulas that need to be solved are produced, memory and data structures are usually limited. For example, arrays in programming languages are usually indexed from 0 to a constant n. Although it is possible to encode finite arrays in the SMT theory of arrays, that would not always be a satisfying solution, one reason being that extensional equality on a finite array from 0 to n cannot be directly modelized using the extensional equality on infinite arrays which considers all integers. An SMT theory of finite sequences, in which the sequences are collections of values indexed over a set of contiguous integers, would simplify the solving of formulas that modelize such data structures. Moreover, finite sequences with concatenation and extraction operators can also be used to express particular specification languages such as separation logic. One difficulty is to choose the set of operations on the sequences to support, since the decidability of the theory depends on them. On the other hand, complete decidability is not always required since the formulas obtained from program verification can have specific shapes or uses of the operations. The objective of the thesis is to study which theory of sequences is appropriate for program verification. Examples from the industry will be available for evaluation. Moreover, generalization of the theory with other codomains (finite sets, finite multi-sets) could also be studied. The evaluation of these theories will be done through implementations in OCaml in the Alt-Ergo SMT solver and the Colibri2 constraint solver.