Symbolic Automatic Relations and Their Applications to SMT and CHC Solving

TL;DR

This paper introduces symbolic automatic relations (SARs), a new method combining symbolic automata and automatic relations, to improve reasoning about recursive data structures in SMT and CHC solving, with a practical satisfiability checker and experimental validation.

Contribution

The paper proposes SARs, a novel framework that extends symbolic automata and automatic relations, enabling automated reasoning about recursive data structures in verification tools.

Findings

The satisfiability problem for SARs is undecidable in general.

A sound, incomplete satisfiability checker for SARs is developed via reduction to CHC solving.

Experimental results demonstrate the effectiveness of the approach in SMT and CHC solving contexts.

Abstract

Despite the recent advance of automated program verification, reasoning about recursive data structures remains as a challenge for verification tools and their backends such as SMT and CHC solvers. To address the challenge, we introduce the notion of symbolic automatic relations (SARs), which combines symbolic automata and automatic relations, and inherits their good properties such as the closure under Boolean operations. We consider the satisfiability problem for SARs, and show that it is undecidable in general, but that we can construct a sound (but incomplete) and automated satisfiability checker by a reduction to CHC solving. We discuss applications to SMT and CHC solving on data structures, and show the effectiveness of our approach through experiments.