Auditorium (IMAG)
31 May 2018 - 14h00
Automated Reasoning in Separation Logic with Inductive Definitions (Phd Defense)
by Cristina Serban from VERIMAG, Université Grenoble Alpes
Abstract: The main contribution of this thesis is a sound and complete proof system for entailments between inductive predicates, which are frequently encountered when verifying programs that work with dynamically allocated recursive data structures. We introduce a generalized proof system for first-order logic, and then adapt it to separation logic, a framework that addresses many of the difficulties posed by reasoning about dynamically allocated heaps. Soundness and completeness are ensured through four semantic restrictions and we also propose a proof-search semi-algorithm that becomes a decision procedure for the entailment problem when the semantic restrictions hold.
This higher-order reasoning about entailments requires first-order decision procedures for the underlying logic when applying inference rules and during proof search. Thus, we provide two decision procedures for separation logic, considering the quantifier-free and the Exists*Forall*-quantified fragments, which were integrated in the open-source, DPLL(T)-based SMT solver CVC4.
Finally, we also give an implementation of our proof system for separation logic, which uses these decision procedures. Given some inductive predicate definitions and an entailment query as input, a warning is issued when one or more semantic restrictions are violated. If the entailment is found to be valid, the output is a proof. Otherwise, one or more counterexamples are provided.
Jury:
- Radu Iosif - CR1, VERIMAG, Directeur de thèse
- Nikos Gorogiannis - Professeur assistant, Middlesex University London, Rapporteur
- Etienne Lozes - Professeur, Université Nice Sophia Antipolis, Rapporteur
- Wei-Ngan Chin - Professeur associé, National University of Singapore, Rapporteur
- Didier Galmiche - Professeur, Université de Lorraine, Examinateur
- Mihaela Sighireanu - Maître de Conférences, Université Paris Diderot, Examinateur
- Mnacho Echenim - Maître de Conférences, ENSIMAG/LIG, Examinateur
