Thesis

Automated Reasoning in Separation Logic with Inductive Definitions

Supervisors: Radu Iosif

Summary:

The motivation behind this thesis stems from verification tasks that check whether a given piece of code conforms to its specification. Properties of a certain state of the program are described through formulae pertaining to a chosen underlying logic, and it is often needed to test whether they hold and, more importantly, whether they entail the target specification. Satisfiability modulo theory (SMT) solvers are commonly used in practice to answer such queries. They are powerful tools due to their ability to combine decision procedures for several different theories.

We want to provide proof systems for entailments encountered when verifying programs that work with recursive data structures. This adds a layer of complexity to the entailment problem, as the formulae describing program states will need to make use of inductively defined predicates characterizing the data structures. Moreover, the programs will use dy- namic allocation to create as many instances of the data as needed. Thus, we are interested in using separation logic to express properties of these programs, as it is a framework that addresses many of the difficulties posed by reasoning about dynamically allocated heaps. The main contribution of this thesis is a sound and complete proof system for entailments between inductively defined predicates. We give a generalized cyclic proof system for first- order logic, which uses the principle of infinite descent to close recurring branches of a proof, and then adapt it to separation logic. In order to ensure soundness and completeness, four semantic restrictions are introduced, and we analyse their decidability and complexity. 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 some inference rules and during proof search. To this end, we introduce two decision procedures for separation logic, considering the quantifier- free and the ∃*∀* -quantified fragments. We study the decidability and complexity of these fragments and show evaluation results of their respective decision procedures, which were integrated in the open-source, DPLL(T)-based SMT solver CVC4.

Finally, we also present an implementation of our proof system for separation logic, which makes use of the above decision procedures in CVC4. Given 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.

Projects

  • SMT-LIB parser - Parser and well-sortedness checker for version 2.6 of SMT-LIB
  • Inductor - Prototype implementation of a proof search algorithm for inductive predicate entailments.

Talks