Journal article

ABDULLA Parosh A., CEDERBERG Jonathan and VOJNAR Tomáš. Monotonic Abstraction for Programs with Multiply-Linked Structures. International Journal of Foundations of Computer Science. 2013, vol. 24, no. 2, pp. 187-210. ISSN 0129-0541. Available from: http://www.worldscientific.com/doi/abs/10.1142/S0129054113400078
Publication language:english
Original title:Monotonic Abstraction for Programs with Multiply-Linked Structures
Title (cs):Monotónní abstrakce pro programy s dynamickými datovými strukturami s více selektory
Pages:187-210
Place:SG
Year:2013
URL:http://www.worldscientific.com/doi/abs/10.1142/S0129054113400078
Journal:International Journal of Foundations of Computer Science, Vol. 24, No. 2, SG
ISSN:0129-0541
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
Annotation
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.
BibTeX:
@ARTICLE{
   author = {A. Parosh Abdulla and Jonathan Cederberg and
	Tom{\'{a}}{\v{s}} Vojnar},
   title = {Monotonic Abstraction for Programs with Multiply-Linked
	Structures},
   pages = {187--210},
   journal = {International Journal of Foundations of Computer Science},
   volume = {24},
   number = {2},
   year = {2013},
   ISSN = {0129-0541},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.en.iso-8859-2?id=10370}
}

Your IPv4 address: 54.225.20.73
Switch to IPv6 connection

DNSSEC [dnssec]