Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference
Ziyi Yang, George Pîrlea, Ilya Sergey
TL;DR
This work addresses the challenge of inductive invariant synthesis in First-Order Logic by proposing FORCE, an ASP-based framework that unifies diverse FO-synthesis techniques and enables efficient, composable invariant inference for distributed systems. Central to FORCE is orthogonal slices, a dynamic pruning strategy that partitions the FO search space and enables incremental pruning through both clause-level and DNF-level reasoning, including pruning via implication graphs and clause-based constraints. The authors demonstrate substantial performance gains over state-of-the-art methods (notably DuoAI) on complex benchmarks like Paxos, and show that FORCE can interoperate with other tools (e.g., Flyvy) to further prune and bound invariants. The work advances practical automated verification by providing a modular, solver-aided approach to FO invariant synthesis with tunable pruning, extendable to a broad class of invariant inference frameworks.
Abstract
We present a framework for synthesising formulas in first-order logic (FOL) from examples, which unifies and advances state-of-the-art approaches for inference of transition system invariants. To do so, we study and categorise the existing methodologies, encoding techniques in their formula synthesis via answer set programming (ASP). Based on the derived categorisation, we propose orthogonal slices, a new technique for formula enumeration that partitions the search space into manageable chunks, enabling two approaches for incremental candidate pruning. Using a combination of existing techniques for first-order (FO) invariant synthesis and the orthogonal slices implemented in our framework FORCE, we significantly accelerate a state-of-the-art algorithm for distributed system invariant inference. We also show that our approach facilitates composition of different invariant inference frameworks, allowing for novel optimisations.