Detail výsledku

Monotonic Abstraction for Programs with Multiply-Linked Structures

CEDERBERG, J.; VOJNAR, T.; ABDULLA, P. Monotonic Abstraction for Programs with Multiply-Linked Structures. INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2013, vol. 24, no. 2, p. 187-210. ISSN: 0129-0541.
Typ
článek v časopise
Jazyk
anglicky
Autoři
Cederberg Jonathan
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Abdulla Parosh
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

URL
Rok
2013
Strany
187–210
Časopis
INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, roč. 24, č. 2, ISSN 0129-0541
DOI
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"
}
Projekty
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, zahájení: 2011-01-01, ukončení: 2015-12-31, ukončen
Práce se složitými datovými strukturami a paralelismem v prostředí Rich Model Toolkit, MŠMT, COST, OC10009, zahájení: 2010-01-01, ukončení: 2012-12-31, řešení
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti, GAČR, Standardní projekty, GAP103/10/0306, zahájení: 2010-01-01, ukončení: 2013-12-31, řešení
Verifikace a optimalizace počítačových systémů, VUT, Vnitřní projekty VUT, FIT-S-12-1, zahájení: 2012-01-01, ukončení: 2014-12-31, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru