Separation-Logic-Prädikate und Hyperkantenersetzungsgrammatiken zur Heapabstraktion 


Die Verifikation von Software mit dynamischen Datenstrukturen erfordert im Allgemeinen den Umgang mit einem unendlichen Zustandsraum. Eine Möglichkeit, diesen auf endliche Größe zu reduzieren, besteht in der Abstraktion des Heaps.
In diesem Vortrag werden die Heapmodellierung durch Hypergraphen in Verbindung mit Hyperkantenersetzungsgrammatiken sowie die Modellierung und Verifikation mittels der Separation Logic behandelt. Grammatiken, die zur Heapabstraktion eingesetzt werden, müssen bestimmte Anforderungen erfüllen. Werden diese auf Separation-Logic-Prädikate übertragen, so lassen sich Regeln für die Abstraktion und das Rearrangement herleiten, die zur Verifikation eingesetzt werden können.