Detail publikace

Monotonic Abstraction for Programs with Multiply-Linked Structures

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

Originální název

Monotonic Abstraction for Programs with Multiply-Linked Structures

Typ

článek v časopise - ostatní, Jost

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

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

Autoři

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

Rok RIV

2013

Vydáno

1. 2. 2013

ISSN

0129-0541

Periodikum

International Journal of Foundations of Computer Science

Ročník

24

Číslo

2

Stát

Singapurská republika

Strany od

187

Strany do

210

Strany počet

24

URL

http://www.worldscientific.com/doi/abs/10.1142/S0129054113400078

BibTex

@article{BUT103515,
  author="Jonathan {Cederberg} and Tomáš {Vojnar} and Parosh {Abdulla}",
  title="Monotonic Abstraction for Programs with Multiply-Linked Structures",
  journal="International Journal of Foundations of Computer Science",
  year="2013",
  volume="24",
  number="2",
  pages="187--210",
  doi="10.1142/S0129054113400078",
  issn="0129-0541",
  url="http://www.worldscientific.com/doi/abs/10.1142/S0129054113400078"
}