Automated Entailment Proving in Separation Logic
Dr Chin Wei Ngan, Associate Professor, School of Computing
COM2 Level 4
Executive Classroom, COM2-04-02
Abstract:
Separation logic has been actively developed in the last two decades as a promising formalism to model and reason about the memory-safety of computer programs. It provides an expressive model of the program states by combining spatial operations, which describe the separation of the memory, and inductive heap predicates, which depict the shapes of recursive data structures, such as linked lists, trees, and graphs. However, this expressiveness also leads to challenges in proving separation logic entailments which are verification conditions introduced in the program reasoning.
In this thesis, we consider the problem of proving entailments in a fragment of symbolic-heap separation logic with user-defined inductive heap predicates. This is one of the most popular separation logic fragments, which has been widely studied and utilized in both academic and industrial research. We propose comprehensive solutions to automatically prove entailments using proof techniques based on mathematical induction. To summarize, this thesis makes the following contributions.
Firstly, we present a mutual induction proof system by proposing a novel induction principle on the size of heap model satisfying multiple goal entailments. This principle allows entailments which are derived in an on-going proof to be used as hypotheses to prove future entailments which will be introduced within the same proof. Since the applicable hypotheses are not limited to only induction hypotheses but also other derived entailments, our presented technique increases the success chance of proving entailments.
Secondly, we introduce a lemma synthesis framework which can automatically synthesize lemmas to assist in proving entailments. More specifically, the framework first discovers necessary lemma templates which have similar heap structure with a goal entailment. Then, it utilizes a structural induction proof system and a template-based constraint solving technique to refine the lemma templates and obtain the desired lemmas. Our framework can synthesize general and modular lemmas to prove sophisticated entailments, which cannot be handled by existing provers.
Finally, we develop a failure learning framework which can systematically learn from the failure of induction hypothesis applications to repair unsuccessful proof attempts. In particular, the framework first identifies unmatchable variables, constants, or pure formulas from the failed induction hypothesis applications. Afterward, it can weaken, generalize, or perform case analysis on the unmatchable components to introduce more potential induction hypotheses or to apply the existing ones. These solutions enable our framework to prove many entailments effectively.
We have implemented the proposed proof techniques in a prototype prover named Songbird and have experimented with it on various literature benchmarks from the separation logic competition SLCOMP-2014 as well as challenging synthetic benchmarks. To date, Songbird can prove most of the entailments and outperforms all state-of-the-art separation logic provers. The proof techniques presented in this thesis have opened up more opportunities to utilize separation logic to verify real-world computer programs automatically.