Detail publikačního výsledku

Monotonic Abstraction for Programs with Multiply-Linked Structures

CEDERBERG, J.; VOJNAR, T.; ABDULLA, P.

Original Title

Monotonic Abstraction for Programs with Multiply-Linked Structures

English Title

Monotonic Abstraction for Programs with Multiply-Linked Structures

Type

Peer-reviewed article not indexed in WoS or Scopus

Original 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.

English 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.

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

Key words in English

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

Authors

CEDERBERG, J.; VOJNAR, T.; ABDULLA, P.

RIV year

2012

Released

28.09.2011

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Volume

2011

Number

6945

State

Federal Republic of Germany

Pages from

125

Pages to

138

Pages count

14

URL

http://www.springerlink.com/content/u75210w230688v22

Full text in the Digital Library

http://hdl.handle.net/

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"
}