期刊
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING
卷 136, 期 -, 页码 -出版社
ELSEVIER SCIENCE INC
DOI: 10.1016/j.jlamp.2023.100906
关键词
Decision procedures; Satisfiability modulo theories; Arrays; Feferman-Vaught; Composition theorems
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.
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/).
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据