Loading...
research article
On algebraic array theories
September 11, 2023
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/).
Type
research article
Web of Science ID
WOS:001080961800001
Authors
Publication date
2023-09-11
Publisher
Volume
136
Article Number
100906
Peer reviewed
REVIEWED
EPFL units
Available on Infoscience
February 14, 2024
Use this identifier to reference this record