Inductive Synthesis of Inductive Heap Predicates
summary
Claim: an algorithm synthesises recursive Separation Logic predicates from concrete heap graphs using positive-only ILP encoded in answer set programming, adding a heap linearity constraint to enforce separating conjunction. It generates predicates with payload constraints (sorted lists, binary search trees) and nested recursion (n-ary trees), includes a memory graph generator to produce positive examples, and evaluates as efficient and correct on benchmarks that exceed prior tools; artifacts and encodings are available.
AI-written summary · about
chapters (9)
- 0:00Inductive heap predicates
- 2:30Separation logic challenges
- 5:19Negative examples in learning
- 6:46Separation logic and logic programming
- 8:14Main results and evaluation
- 8:55Answer Set Programming for synthesis
- 10:24Summary and tool applications
- 10:46Q&A: Predicate strength
- 12:14Q&A: Disjunctions in separation logic
related talks
22mA Calculus of Inductive Linear Constructions
23mInductive Program Synthesis by Meta-Analysis-Guided Hole Filling
22mImplementing separation logic using an SMT-backed Frame Rule
19mType Inference Logics
17mCalculational design of Incorrectness Separation Logic
25mRecursive Program Synthesis using Paramorphisms
18mMobius: Synthesizing Relational Queries with Recursive and Invented Predicates
05mNew foundations for probabilistic separation logic