Automated Tools for Inductive Reasoning in Separation Logic
Friday 30 January 2026 at 14h00
ENS Paris-Saclay, Amphi 1B26 and online
Abstract: The automated program verification aims to produce formal proofs of correctness for programs with respect to their specifications, requiring minimal user interaction. This technique is based on expressive program logics to capture the properties of programs, and algorithms or heuristics to decide satisfiablity and entailment problem for these logics. Separation logic is one of such logics, specifically designed for reasoning about programs that dynamically allocate memory and mutate this memory through pointers. To specify unbounded memory regions, separation logic includes user-defined predicates, usually expressed through inductive rules. The satisfiability and entailment problems are undecidable in general, but they are decidable for specific fragments. For instance, the PCE fragment is a restriction of the symbolic heap fragment, for which the satisfiability is decidable, where the inductively defined predicates satisfy some syntactic and semantic constraints.
This thesis proposes two extensions of the PCE fragment. The first extension defines a fragment, including the PCE one and formulæ that, although non-PCE, specify data structures that could be represented by PCE formulæ. We propose a procedure attempting to compute an equivalent PCE representation of non-PCE formulæ. We implemented this procedure and tested it on a benchmark of SL formulæ. The second extension supports the specification of overlaid data structures, i.e., data structures that share an unbounded set of locations and are therefore difficult to capture using separating conjunction. The extension, called OSL, introduces an additional operator, the overlaid separating conjunction ✪, which allows for composing heaps that share locations as long as they allocate them with distinct fields. We demonstrate that the OSL fragment has a decidable satisfiability problem.
The defense will be in English.
Jury:
- Radu IOSIF, DR CNRS, Vérimag (Reviewer)
- Florian ZULEGER, Associate Professor, TU Wien(Reviewer)
- Viktor KUNCAK, Associate Professor, EPFL (Examiner)
- Étienne LOZES, Professor, Université Cote d’Azur (Examiner)
- Adam ROGALEWICZ, Associate Professor, Brno University of Technology (Examiner)
- Nicolas Peltier, CR CNRS, LIG (co-advisor)
- Mihaela Sighireanu, Professor, ENS Paris-Saclay (co-advisor)