Verifikation von Zeigerprogrammen

点击翻译按钮获取中文摘要

Die Entwicklung und insbesondere die Verifikation von Programmen mit Zeigern ist weiterhin eine große Herausforderung an existierende Methoden. Ziel dieses Projekts ist die Entwicklung von Verifikationstechniken und einer Verifikationsumgebung für imperative Programme mit Zeigern. Dazu sollen die Ergebnisse des ersten Projektabschnitts von Schleifen auf Prozeduren und Objektorientierung verallgemeinert werden. Die Verifikationsumgebung (in Isabelle/HOL) soll nicht für eine existierende Programmiersprache ausgelegt werden, sondern für eine minimale objektorientierte Sprache: damit einem nicht die barocken Auswüchse etwa von C (und leider auch von Java) den Blick verstellen, damit man sich bei der Verifikation auf das eigentliche algorithmische Problem konzentrieren kann und damit die Prinzipien für andere Forscher so klar wie möglich erkennbar sind. Innerhalb dieser Verifikationsumgebung sollen zwei konkurrierende Ansätze, Multi-Heaps und Separation Logik, bezüglich ihrer Eignung sowohl bei der Spezifikation als auch der Verifikation an Hand substanzieller Fallstudien miteinander verglichen werden.