PhD Defense

Theory of Sequences
Tailored for Program Verification

By Hichem Rami AIT EL HARA

I will defend my PhD thesis on October 15th, 2025 at 14h00, in Amphi 33 - CEA Nano-INNOV Building 862 - 1st floor 2, boulevard Thomas Gobert 91120 Palaiseau France.
The entrance (for externals) to the site is from Sent. de Corbeville (on OSM), for more info on how to get there click here.

The defense will be retransmitted online on Livestorm.

If you're planning to attend in person please let me know by filling out this form: https://framadate.org/XBMZNfCje613Bu3I. (Note: If you are not a EU citizen, please email me at hra687261(at)gmail.com so that I can make sure you can access the site)

Both the slides and the presentation will be in English.

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.