An encoding of array verification problems into array-free Horn clauses

TL;DR

This paper introduces a novel method for verifying array properties by encoding array verification problems into array-free Horn clauses, enabling the use of existing solvers for safety verification.

Contribution

It presents a new encoding technique that transforms array verification into scalar Horn clause problems, avoiding the need for new abstract domains or interpolation methods.

Findings

Successfully verified the functional correctness of selection sort.

The encoding produces nonlinear Horn problems with tree unfoldings.

The approach leverages existing Horn clause solvers for array verification.

Abstract

Automatically verifying safety properties of programs is hard, and it is even harder if the program acts upon arrays or other forms of maps. Many approaches exist for verifying programs operating upon Boolean and integer values (e.g. abstract interpretation, counterexample-guided abstraction refinement using interpolants), but transposing them to array properties has been fraught with difficulties.In contrast to most preceding approaches, we do not introduce a new abstract domain or a new interpolation procedure for arrays. Instead, we generate an abstraction as a scalar problem and feed it to a preexisting solver, with tunable precision.Our transformed problem is expressed using Horn clauses, a common format with clear and unambiguous logical semantics for verification problems. An important characteristic of our encoding is that it creates a nonlinear Horn problem, with tree unfoldings, even though following "flatly" the control-graph structure ordinarily yields a linear Horn problem, with linear unfoldings. That is, our encoding cannot be expressed by an encoding into another control-flow graph problem, and truly leverages the capacity of the Horn clause format.We illustrate our approach with a completely automated proof of the functional correctness of selection sort.