CHC-Based Verification of Programs Through Graph Decompositions

We present a novel methodology for automated program analysis that leverages graph encodings of computations. The crux of our approach lies in restructuring the program behavior graphs through tree decompositions of bounded width. To achieve this, we introduce a notion of labeled multigraph, called nested-word shape, that is used as a summary for portions of program behavior graphs. Such multigraphs are used within the construction of a symbolic data-tree automaton (sdta), a recently introduced notion of automaton designed to accept tree data structures. We use sdtas to capture the tree decompositions of the program behavior graphs of a given program. Verification of the original program is then accomplished by checking the emptiness of the data-tree language accepted by these sdtas, which can be effectively reduced to the satisfiability of constrained Horn clauses (CHC). Our approach results in an under-approximate analysis parameterized by the width k of the tree decomposition used for the analysis, and thus provides a complete method for the classes of programs whose behavior graphs have bounded treewidth. We detail our methodology for recursive sequential programs, which enjoy the bounded treewidth property, and subsequently extend it to concurrent programs. Notably, our approach shows promise across an even broader spectrum of program classes, including distributed systems and concurrent programs operating under weak memory models.