Automatic Reasoning for the Modular Verification of Programs using Complex Data Structures

Supervisors: Radu Iosif, Nicolas Halbwachs

Abstract: The objective of my PhD thesis is to develop tools for automatic reasoning in separation logic - an abstract framework which allows for modular analysis - using decidability and complexity results from automata theory. More precisely, the theory of tree automata is applied in order to solve problems such as satisfiability and validity in separation logic, in the context of shape analysis. Once these problems are overcome, we will extend the reasoning to the data contained in the memory cells, through modular verification techniques, which involve processes such as bi-abduction (the inference of anti-frames and frames for an implication) or rely-guarantee (the inference of abstract environments for multi-thread programs).


  • Parse SMT-LIB - Parser and well-sortedness checker for version 2.6 of SMT-LIB