On Automated Lemma Generation for Separation Logic with Inductive Definitions

TL;DR

This paper introduces an automatic lemma generation method for separation logic with inductive definitions, enhancing the verification of programs manipulating complex data structures.

Contribution

It presents a novel, syntactic, and deterministic approach for generating lemmas, improving verification of iterative and recursive programs with complex data structures.

Findings

Effective on sophisticated benchmarks like balanced trees and search algorithms

Handles iterative procedures for data structure manipulation

Demonstrates efficiency and power in automated verification tasks

Abstract

Separation Logic with inductive definitions is a well-known approach for deductive verification of programs that manipulate dynamic data structures. Deciding verification conditions in this context is usually based on user-provided lemmas relating the inductive definitions. We propose a novel approach for generating these lemmas automatically which is based on simple syntactic criteria and deterministic strategies for applying them. Our approach focuses on iterative programs, although it can be applied to recursive programs as well, and specifications that describe not only the shape of the data structures, but also their content or their size. Empirically, we find that our approach is powerful enough to deal with sophisticated benchmarks, e.g., iterative procedures for searching, inserting, or deleting elements in sorted lists, binary search tress, red-black trees, and AVL trees, in a very efficient way.