20.12.2012, Nie mehr Segmentation Faults dank Shape Analyse

Shape Analyse ist eine statische Programmanalyse, die Eigenschaften von dynamisch allokierten Datenstrukturen wie Listen entdeckt und verifiziert. Beispiele für Eigenschaften, die wir im Vortrag betrachten, sind Abwesenheit von Speicherfehlern wie mehrfach oder gar nicht freigegebener Speicher oder auch die Korrektheit von Sortieralgorithmen auf Listen. Wir begeben uns auf eine Reise von den Ursprüngen der Shape Analyse über den historischen Durchbruch von Sagiv, Reps und Wilhelm basierend auf dreiwertiger Logik bis hin zu modernen Analysen basierend auf Separation Logic. Insbesondere finden die Beiträge des Vortragenden Berücksichtigung. Wir schließen mit einem Blick auf die aktuellen Herausforderungen dieses spannenden Forschungsfeldes.