Termination analysis of procedural pointer programs modelled by graph grammars

Khalifa, Mohamed; Noll, Thomas; Fesefeldt, Ira Justus; Katoen, Joost-Pieter

doi:10.18154/RWTH-2022-09096

Termination analysis of procedural pointer programs modelled by graph grammars

Khalifa, Mohamed^RWTH*

2022

VerantwortlichkeitsangabeMohamed Khalifa

ImpressumAachen : RWTH Aachen University 2022

Umfang1 Online-Ressource : Diagramme

Masterarbeit, RWTH Aachen University, 2022

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Noll, Thomas (Thesis advisor)^RWTH* ; Katoen, Joost-Pieter (Thesis advisor)^RWTH* ; Fesefeldt, Ira Justus (Consultant)^RWTH*

Tag der mündlichen Prüfung/Habilitation
2022-09-08

Online
DOI: 10.18154/RWTH-2022-09096
URL: https://publications.rwth-aachen.de/record/853842/files/853842.pdf

Einrichtungen

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Predicate Abstraction Analysis is a data-flow analysis of pointer programs operating on heaps modelled as hypergraphs. The semantics of pointer programs utilises hyperedge replacement grammars as an abstraction mechanism, thereby providing a compact representation of programs in the form of abstract transition systems. The analysis propagates information about graph predicates, which is used to prove the termination of programs under certain conditions. We extend the analysis to procedural and, in particular, recursive pointer programs and show that the soundess of the analysis is preserved under the extended setting.

OpenAccess:
PDF