% IMPORTANT: The following is UTF-8 encoded. This means that in the presence
% of non-ASCII characters, it will not work with BibTeX 0.99 or older.
% Instead, you should use an up-to-date BibTeX implementation like “bibtex8” or
% “biber”.
@PHDTHESIS{Jansen:708116,
author = {Jansen, Christina},
othercontributors = {Katoen, Joost-Pieter and Huisman, Marieke and Noll, Thomas},
title = {{S}tatic {A}nalysis of {P}ointer {P}rograms - {L}inking
{G}raph {G}rammars and {S}eparation {L}ogic},
school = {RWTH Aachen University},
type = {Dissertation},
address = {Aachen},
reportid = {RWTH-2017-09657},
pages = {1 Online-Ressource (xi, 286 Seiten) : Diagramme},
year = {2017},
note = {Veröffentlicht auf dem Publikationsserver der RWTH Aachen
University; Dissertation, RWTH Aachen University, 2017},
abstract = {This thesis presents a sound abstraction framework for the
static analysis of pointer programs, which is able to handle
(recursive) procedures as well as concurrency. The framework
builds on a graph representation of the heap using so-called
hypergraphs. In these graphs edges are labelled and can be
connected to arbitrarily many vertices. Understanding edges
between two vertices as pointers and the remaining edges as
placeholders for parts of the heap, hypergraphs feature the
necessary concepts for heap abstraction. More concretely,
edge labels are used to specify the shape of the heap that
is abstracted. Hyperedge replacement grammars formalise this
mapping. That is, they define the data structures each of
the labels represents. Concretisation and abstraction of
heaps then directly correspond to forward and backward
application of production rules of the hyperedge replacement
grammar, respectively. The first part of the thesis lays the
formal foundation for hypergraph-based heap representation
and its concretisation and abstraction. Utilising this, an
analysis approach for non-procedural pointer programs is
presented. Additionally, we make requirements of hyperedge
replacement grammars that are crucial for the soundness and
termination of concretisation and abstraction. It is shown
that each hyperedge replacement grammar can be transformed
such that it satisfies these requirements. In the second
part of the thesis, a bridge between hyperedge replacement
grammars and the symbolic heap fragment of Separation Logic
is built. In particular, a translation procedure between
both formalisms is given and proven correct. Additionally,
we provide the Separation Logic counterparts of the
requirements determined in the preceding part and show that
they are preserved by the translation. The relationship
between Separation Logic and hyperedge replacement grammars
inspired the extension to a framework that modularly handles
procedures and fork-join-concurrency. That is, in the last
part of the thesis we adopt the concept of contracts, i.e.
pairs consisting of a pre- and a postcondition that capture
the effect of a procedure or thread execution, to obtain
procedure and thread modular analyses, respectively. In the
latter case, we additionally introduce permissions to
hypergraphs. They constitute a concept which is, similarly
to contracts, well-understood for Separation Logic.
Permissions provide transferable access grants to heap parts
and enable the analysis of threads independently of each
other. As a main contribution of the procedural and
concurrent program analysis, a novel approach for automated
derivation of procedure and (permission-enriched) thread
contracts is presented.},
cin = {120000 / 121310},
ddc = {530},
cid = {$I:(DE-82)120000_20140620$ / $I:(DE-82)121310_20140620$},
pnm = {CARP - Correct and Efficient Accelerator Programming
(287767)},
pid = {G:(EU-Grant)287767},
typ = {PUB:(DE-HGF)11},
doi = {10.18154/RWTH-2017-09657},
url = {https://publications.rwth-aachen.de/record/708116},
}
Gast ::