On algebraic array theories

Automatic verification of programs manipulating arrays relies on specialised decision procedures. A methodology to classify the theories handled by these procedures is introduced. It is based on decomposition theorems in the style of Feferman and Vaught. The method is applied to obtain an extension of combinatory array logic that is closed under propositional operations and Hoare triples. A classification according to expressiveness of six different fragments studied in the literature is given.(c) 2023 The Author(s). Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons .org /licenses /by /4 .0/).

Automated summary

This article introduces a methodology based on decomposition theorems to classify the theories handled by specialized decision procedures for automatic verification of programs manipulating arrays. It further applies this method to obtain an extension of combinatory array logic. The article also provides a classification of six different fragments based on their expressiveness.