ADCL: Acceleration Driven Clause Learning for Constrained Horn Clauses

TL;DR

This paper introduces ADCL, a new calculus for solving Constrained Horn Clauses that leverages acceleration techniques to significantly shorten proofs, improving automated program verification efficiency.

Contribution

The paper presents ADCL, a novel calculus that integrates acceleration methods into clause learning for CHC satisfiability, implemented in the LoAT tool.

Findings

ADCL reduces proof lengths in CHC satisfiability checks.

Empirical evaluation shows ADCL outperforms existing tools.

Acceleration techniques effectively improve static program analysis.

Abstract

Constrained Horn Clauses (CHCs) are often used in automated program verification. Thus, techniques for (dis-)proving satisfiability of CHCs are a very active field of research. On the other hand, acceleration techniques for computing formulas that characterize the N-fold closure of loops have successfully been used for static program analysis. We show how to use acceleration to avoid repeated derivations with recursive CHCs in resolution proofs, which reduces the length of the proofs drastically. This idea gives rise to a novel calculus for (dis)proving satisfiability of CHCs, called Acceleration Driven Clause Learning (ADCL). We implemented this new calculus in our tool LoAT and evaluate it empirically in comparison to other state-of-the-art tools.