Termination analysis of procedural pointer programs modelled by graph grammars

Khalifa, Mohamed; Noll, Thomas (Thesis advisor); Katoen, Joost-Pieter (Thesis advisor); Fesefeldt, Ira Justus (Consultant)

Aachen : RWTH Aachen University (2022)
Master Thesis

Masterarbeit, RWTH Aachen University, 2022

Abstract

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.