Forest automata for verification of heap manipulation
Forest automata for verification of heap manipulation
复制标题
用于验证堆操作的森林自动机
DOI：
10.1007/s10703-012-0150-8
复制
发表时间：
2011
影响因子：
0.8
通讯作者：
Tomáš Vojnar
中科院分区：
文献类型：
--
作者：
P. Habermehl;L. Holík;Adam Rogalewicz;Jirí Simácek;Tomáš Vojnar
我们考虑对操纵动态链接的数据结构的程序的验证，例如各种形式的单一和双关联列表或树，我们考虑了这种系统的重要属性，例如无零件的垃圾，没有垃圾，形状属性等。基于对树自动机的新颖使用来形成堆配置。堆的一部分是指它们的边界，我们允许树的字母包含其他嵌套的树自动机，可以使堆的层次表示在所谓的抽象常规树模型检查中，允许基于符号状态探索的程序以及可改进的抽象。基于分离的方法（效率）的一些优点。
We consider verification of programs manipulating dynamic linked data structures such as various forms of singly and doubly-linked lists or trees. We consider important properties for this kind of systems like no null-pointer dereferences, absence of garbage, shape properties, etc. We develop a verification method based on a novel use of tree automata to represent heap configurations. A heap is split into several “separated” parts such that each of them can be represented by a tree automaton. The automata can refer to each other allowing the different parts of the heaps to mutually refer to their boundaries. Moreover, we allow for a hierarchical representation of heaps by allowing alphabets of the tree automata to contain other, nested tree automata. Program instructions can be easily encoded as operations on our representation structure. This allows verification of programs based on symbolic state-space exploration together with refinable abstraction within the so-called abstract regular tree model checking. A motivation for the approach is to combine advantages of automata-based approaches (higher generality and flexibility of the abstraction) with some advantages of separation-logic-based approaches (efficiency). We have implemented our approach and tested it successfully on multiple non-trivial case studies.