Parameterized Verification under TSO with Data Types

被引：2

作者：

Abdulla, Parosh Aziz ^{[1
]}

Atig, Mohamad Faouzi ^{[1
]}

Furbach, Florian ^{[1
]}

Godbole, Adwait A. ^{[3
]}

Hendi, Yacoub G. ^{[1
]}

Krishna, Shankara N. ^{[2
]}

Spengler, Stephan ^{[1
]}

机构：

[1] Uppsala Univ, Uppsala, Sweden

[2] Indian Inst Technol, Mumbai, Maharashtra, India

[3] Univ Calif Berkeley, Berkeley, CA USA

来源：

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, TACAS 2023 | 2023年 / 13993卷

关键词：

MODEL CHECKING; SYSTEMS; ABSTRACTION; AUTOMATA;

D O I：

10.1007/978-3-031-30823-9_30

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially infinite domains. We present a framework that translates the reachability problem for such systems to the reachability problem for register machines enriched with the given abstract data type. We use the translation to obtain tight complexity bounds for TSO-based parameterized verification over several abstract data types, such as push-down automata, ordered multi push-down automata, one-counter nets, one-counter automata, and Petri nets. We apply the framework to get complexity bounds for higher order stack and counter variants as well.

引用

页码：588 / 606

页数：19

共 48 条

[1] Regular model checking [J].

Parosh Aziz Abdulla .

International Journal on Software Tools for Technology Transfer, 2012, 14 (2) :109-118

[2]

Abdulla P. A., 2018, Handbook of Model Checking, P685, DOI [DOI 10.1007/978-3-319-10575-8, 10.1007/978-3-319-10575-8_21, DOI 10.1007/978-3-319-10575-821]

[3] Algorithmic analysis of programs with well quasi-ordered domains [J].