Verification of pointer programs

With this dissertation we present an abstraction and verification framework for pointer programs operating on unbounded heaps. To this end, we introduce two different abstraction methods for pointer-manipulating programs: an abstraction technique for singly-linked structures that guarantees a finite abstract semantics for any given program and a more general approach, employing context-free hyperedge replacement graph grammars to model the data structures and compute the abstraction mappings. The graph grammars are user defined and therefore this approach can handle a variety of different data structures. By means of partial concretization steps we avoid the necessity for explicitly defining the effect of pointer-manipulating operations on abstracted parts of the heap: it is obtained "for free" by combining partial concretization, the concrete pointer operation, and re-abstraction of the transformed state. Besides the possibility to check for pointer safety, assuring the absence of null dereferences, and shape safety, the preservation of the data structure, we establish an expressive pointer logic that is based on LTL. It allows to specify safety as well as liveness properties for the executions of the system. We show that the corresponding model checking problem can be reduced to an LTL model checking problem enabling the application of existing, highly optimized model checkers. We show the practical feasibility of our approach by applying it to the well-known Deutsch-Schorr-Waite traversal algorithm for binary trees – a stackless traversal algorithm that uses destructive updates. Finally, we introduce an extension of our framework to concurrent pointer programs with unbounded thread creation. For that purpose we model the control-flow and heap semantics separately as Petri nets. Abstracting the heap only, we obtain a data-abstract semantics for which we can show that the model checking problem is decidable. To obtain practically feasible results, however, we are forced to apply in a second step abstraction to the control-flow semantics as well. It turns out that the resulting Petri net can be represented as a finite transition system, to that our model checking method can be applied.

Grantor dc:publisher

Publikationsserver der RWTH Aachen University

Year dc:date

2009

Author dc:creator

• Rieger, Stefan

Contributors dc:contributor

• Katoen, Joost-Pieter

• info:eu-repo/classification/ddc/004
• Zeiger <Informatik>
• Verifikation
• Model Checking
• Abstraktion
• Graph-Grammatik
• Hypergraph
• Graphersetzungssystem
• Informatik
• hyperedge replacement grammar
• pointer programs
• verification
• heap abstraction

Statement dc:rights

• info:eu-repo/semantics/openAccess

Language dc:language

eng

Identifier

https://publications.rwth-aachen.de/search?p=id:%22RWTH-CONV-113647%22

OAI record oai:identifier

https://publications.rwth-aachen.de/oai2d?verb=GetRecord&metadataPrefix=oai_dc&identifier=oai%3Apublications.rwth-aachen.de%3A51346