Inductive Synthesis of Inductive Heap Predicates

Learn about an innovative approach to automatically synthesizing recursive predicates in Separation Logic from concrete data structure instances using Inductive Logic Programming techniques in this 13-minute conference presentation. Discover how researchers Ziyi Yang and Ilya Sergey from the National University of Singapore tackle the key challenges of making predicate synthesis effective without requiring negative examples and enabling summarization of both heap shape and data properties. Explore their novel predicate learning algorithm that formulates ILP-based learning using only positive examples and synthesizes property-rich Separation Logic predicates from concrete memory graphs. Examine how this framework efficiently synthesizes predicates for complex structures previously beyond state-of-the-art tools, including binary search trees with non-trivial payload constraints and n-ary trees with nested recursion. Understand the practical applications through their memory graph generator that produces positive heap examples from programs and see how this approach facilitates deductive verification and synthesis of correct-by-construction code, with comprehensive artifacts available for replication and further research.