Algorithmic analysis of array-accessing programs
Algorithmic analysis of array-accessing programs
复制标题
DOI：
10.1145/2287718.2287727
复制
发表时间：
2009-09
期刊：
影响因子：
--
通讯作者：
R. Alur;Pavol Cerný;S. Weinstein
中科院分区：
文献类型：
--
作者：
R. Alur;Pavol Cerný;S. Weinstein
对于数据变量遍及布尔域或有限域的程序来说，程序验证是可解的，这也是近期软件模型检查工具的基础。在本文中，我们将考虑对使用布尔变量的程序进行算法验证，此外，这些程序还访问一个长度可能无界、元素遍及无界数据域的单一只读数组。我们证明，虽然可达性问题在一般情况下无法判定，但 (1) 对于访问数组的 for 循环没有嵌套的程序来说，可达性问题是 Pspace-complete；(2) 对于具有双嵌套循环的受限类程序来说，可达性问题是可判定的。第二个结果与自动机和定义数据字语言的逻辑建立了联系。
For programs whose data variables range over Boolean or finite domains, program verification is decidable, and this forms the basis of recent tools for software model checking. In this article, we consider algorithmic verification of programs that use Boolean variables, and in addition, access a single read-only array whose length is potentially unbounded, and whose elements range over an unbounded data domain. We show that the reachability problem, while undecidable in general, is (1) Pspace-complete for programs in which the array-accessing for-loops are not nested, (2) decidable for a restricted class of programs with doubly nested loops. The second result establishes connections to automata and logics defining languages over data words.