Monotonic Abstraction for Programs with Multiply-Linked Structures
Monotonic Abstraction for Programs with Multiply-Linked Structures
复制标题
具有多重链接结构的程序的单调抽象
DOI：
10.1142/s0129054113400078
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Tomáš Vojnar
中科院分区：
文献类型：
--
作者：
P. Abdulla;Jonathan Cederberg;Tomáš Vojnar
我们调查使用单调抽象和向后可达性分析的手段进行形状分析的程序与多点结构。通过将堆编码为顶点和边标记的图，我们可以对用C编程语言编写的程序所表现出的低级行为进行建模。使用签名的概念，它是定义堆集合的谓词，我们可以检查诸如空指针解引用和形状不变等属性。我们报告的结果，从运行一个原型的方法的基础上，几个程序，如插入和合并的双向链表。
We investigate the use of monotonic abstraction and backward reachability analysis as means of performing shape analysis on programs with multiply pointed structures. By encoding the heap as a vertex- and edge-labeled graph, we can model the low level behaviour exhibited by programs written in the C programming language. Using the notion of signatures, which are predicates that define sets of heaps, we can check properties such as absence of null pointer dereference and shape invariants. We report on the results from running a prototype based on the method on several programs such as insertion into and merging of doubly-linked lists.