Inductive Synthesis of Inductive Heap Predicates -- Extended Version

TL;DR

This paper introduces a novel ILP-based method for automatically synthesizing rich recursive predicates in Separation Logic from positive heap examples, enabling analysis of complex data structures like trees and lists.

Contribution

It presents a positive-only ILP learning algorithm for heap predicates, capable of handling complex structures and data properties, advancing automated heap analysis.

Findings

Successfully synthesizes predicates for complex data structures.

Handles non-trivial payload constraints and nested recursion.

Facilitates deductive verification and correct-by-construction synthesis.

Abstract

We present an approach to automatically synthesise recursive predicates in Separation Logic (SL) from concrete data structure instances using Inductive Logic Programming (ILP) techniques. The main challenges to make such synthesis effective are (1) making it work without negative examples that are required in ILP but are difficult to construct for heap-based structures in an automated fashion, and (2) to be capable of summarising not just the shape of a heap (e.g., it is a linked list), but also the properties of the data it stores (e.g., it is a sorted linked list). We tackle these challenges with a new predicate learning algorithm. The key contributions of our work are (a) the formulation of ILP-based learning only using positive examples and (b) an algorithm that synthesises property-rich SL predicates from concrete memory graphs based on the positive-only learning. We show that our framework can efficiently and correctly synthesise SL predicates for structures that were beyond the reach of the state-of-the-art tools, including those featuring non-trivial payload constraints (e.g., binary search trees) and nested recursion (e.g., n-ary trees). We further extend the usability of our approach by a memory graph generator that produces positive heap examples from programs. Finally, we show how our approach facilitates deductive verification and synthesis of correct-by-construction code.