Programmiersprachen und Übersetzer

Automatisierte Verifikation von low-level Zeigerprogrammen

Bei der Verifikation von C-Programmen kann die Behandlung von Zeigern bislang nur teilweise automatisiert werden. Tatsächlich muss für gute Ergebnisse die Annahme getroffen werden, dass Zeiger stets auf disjunkte Records auf dem Heap verweisen (Burstalls Speichermodell).

Damit sind jedoch viele idiomatische Verwendungen von C ausgeschlossen: Zeiger auf lokale Variablen, auf Felder von Structs oder auf Teile von Arrays werden häufig an Funktionen übergeben, sie können allerdings nicht formalisiert werden.

Wir haben daher den Ansatz der Lightweight Separation entwickelt. Dieser erlaubt es, beliebige Speicherlayouts zu definieren und deren Eigenschaften in speziellen automatischen Beweisverfahren bei der Verifikation von Programmen zu berücksichtigen.

Der nächste Schritt besteht in der Übertragung auf die objekt-orientierte Programmierung in C++. Neu hinzu kommen hier die Aspekte der Encapsulation und Klasseninvarianten, sowie der Templates als ausdrucksstarkes Mittel der Wiederverwendung.

Ansprechpartner: Holger Gast

Adresse

Prof. Dr. Herbert Klaeren

Universität Tübingen

Wilhelm-Schickard-Institut für Informatik

Jasminweg 21

72076 Tübingen

GERMANY

Anbieterkennung Last modified: Di 21 Nov 2023 12:19:02 CET