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.

翻译：本文提出一种利用归纳逻辑编程技术，从具体数据结构实例中自动合成分离逻辑递归谓词的方法。实现此类有效合成的主要挑战在于：(1) 无需ILP所需的负例即可工作（而基于堆结构的负例难以自动构建），(2) 不仅能概括堆的形态特征（如链表结构），还能归纳其所存储数据的属性特征（如有序链表）。我们通过新型谓词学习算法应对这些挑战。本工作的核心贡献包括：(a) 建立仅使用正例的ILP学习框架，(b) 基于纯正例学习实现从具体内存图合成富含属性的分离逻辑谓词的算法。实验表明，本框架能高效准确地合成当前最先进工具无法处理的复杂结构对应的分离逻辑谓词，包括具有非平凡负载约束的结构（如二叉搜索树）和嵌套递归结构（如n叉树）。我们进一步通过内存图生成器扩展了方法的实用性，该生成器可从程序中自动产生正例堆样本。最后，我们展示了本方法如何促进演绎验证及构造正确性代码的合成。