Solving Constrained Horn Clauses over ADTs by Finite Model Finding

TL;DR

This paper introduces a method for automatically inferring invariants of programs manipulating algebraic data types using tree automata and finite model finders, offering a more practical alternative to first-order logic-based approaches.

Contribution

It proposes a novel automata-based approach for invariant inference over ADTs, demonstrating improved practicality and expressiveness compared to existing first-order logic methods.

Findings

Automata-based invariants can express more complex properties.

The approach is less expensive computationally.

It outperforms state-of-the-art first-order logic engines.

Abstract

First-order logic is a natural way of expressing the properties of computation, traditionally used in various program logics for expressing the correctness properties and certificates. Subsequently, modern methods in the automated inference of program invariants progress towards the construction of first-order definable invariants. Although the first-order representations are very expressive for some theories, they fail to express many interesting properties of algebraic data types (ADTs). Thus we propose to represent program invariants regularly with tree automata. We show how to automatically infer such regular invariants of ADT-manipulating programs using finite model finders. We have implemented our approach and evaluated it against the state-of-art engines for the invariant inference in first-order logic for ADT-manipulating programs. Our evaluation shows that automata-based representation of invariants is more practical than the one based on first-order logic since invariants are capable of expressing more complex properties of the computation and their automatic construction is less expensive.