Publication Details

Monotonic Abstraction for Programs with Multiply-Linked Structures

CEDERBERG, J.; VOJNAR, T.; ABDULLA, P. Monotonic Abstraction for Programs with Multiply-Linked Structures. Lecture Notes in Computer Science, 2011, vol. 2011, no. 6945, p. 125-138. ISSN: 0302-9743.
Czech title
Monotónní abstrakce pro programy s dynamickými datovými strukturami s více selektory
Type
journal article
Language
English
Authors
Cederberg Jonathan
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Abdulla Parosh
URL
Keywords

formal verification, program analysis, upward closed sets, monotonic abstraction, dynamic memory, pointers, dynamic linked data structures, multiple selectors, doubly-linked lists, trees, null pointer dereference, dangling pointers, memory leakage

Abstract

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.

Published
2011
Pages
125–138
Journal
Lecture Notes in Computer Science, vol. 2011, no. 6945, ISSN 0302-9743
BibTeX 
@article{BUT76409,
  author="Jonathan {Cederberg} and Tomáš {Vojnar} and Parosh {Abdulla}",
  title="Monotonic Abstraction for Programs with Multiply-Linked Structures",
  journal="Lecture Notes in Computer Science",
  year="2011",
  volume="2011",
  number="6945",
  pages="125--138",
  issn="0302-9743",
  url="http://www.springerlink.com/content/u75210w230688v22"
}
Back to top