Answer Set Programming for Synthesis, Inference, and Search

Abstract:

Formal specifications are the bedrock of reliable software systems, yet writing them remains notoriously difficult. It requires a dual expertise: deep knowledge of the system being specified and fluency in the rigid logical formalisms of formal methods. This Specification Bottleneck manifests in two dimensions: the Discovery Problem, where the correct invariants need to be inferred from examples; and the Modelling Problem, where even a conceptually understood problem must be encoded in a solver-friendly form. This thesis addresses both dimensions of the Specification Bottleneck: it uses Answer Set Programming (ASP) to tackle the Discovery Problem in formal methods, and addresses the Modelling Problem for ASP itself.

Chapter 3 and Chapter 4 address the Discovery Problem through inductive synthesis and inference. Sippy automatically synthesises recursive predicates for heap-manipulating data structures directly from memory instances. By encoding the hypothesis space and domain-specific pruning rules as an ASP problem, Sippy efficiently discovers both the structural shape and the data invariants of the target predicate, improving over prior shape analysis tools on the evaluated benchmark data structures. FORCE addresses the inference of logical invariants for distributed protocols. It introduces a unified taxonomy of existing inference approaches and a novel orthogonal slices technique, which partitions the exponentially large search space into manageable chunks amenable to incremental ASP-based pruning. FORCE demonstrates significant performance improvements over state-of-the-art invariant inference tools on non-trivial distributed protocols.

Chapter 5 addresses the Modelling Problem---an irony that emerges from the preceding two chapters: ASP, our chosen solution, is itself subject to the Specification Bottleneck, since encoding complex constraints directly in ASP requires expertise in stable model semantics and is opaque and error-prone. Crucially, this Modelling Problem is not unique to ASP---the same bottleneck afflicts SAT, where even conceptually simple constraints demand manual, error-prone compilation to Conjunctive Normal Form. SetLah! is a semi-declarative language that resolves this bottleneck for ASP, and in doing so offers a higher-level alternative to direct ASP or CNF encodings. It allows users to express combinatorial search problems using arbitrary First-Order Logic constraints within a structured, block-based syntax, and automatically compiles these into efficient ASP programs, bridging the gap between classical logic and solver-level encodings. Experiments across diverse benchmarks show that, with the efficient ASP system Clingo as the backend, SetLah! programs are competitive with, and often faster than, selected SAT-based tools.

The three contributions are unified by the thesis statement: Chapter 3 and Chapter 4 use ASP to address the Specification Bottleneck in formal methods---the former for heap data structures, the latter for distributed protocol invariants; and Chapter 5 tackles the Specification Bottleneck of ASP itself, making the engine that the first two chapters rely on accessible to non-experts.