Dr. Jan Schwinghammer

"Programmlogik für Sprachen mit höherstufigem Zustand"

Zusammenfassung: Traditionelle Methoden zur Programmverifikation legen ein Speichermodell zugrunde, das erststufig ist, also Werte von Basistypen wie int oder char sowie Zeiger darauf umfasst. Realistische Programmiersprachen hingegen erlauben häufig höherstufigen Zustand, beispielsweise Referenzen (über prozeduralen Typen) in Standard ML oder Zeiger auf Code in C.

In diesem Vortrag werde ich eine Hoare-Logik vorstellen, die die modulare Verifkation von Programmen mit höherstufigem Zustand erlaubt. Ausgehend von den semantischen Grundlagen werde ich die Essenz der Beweisregeln dieser Logik erläutern.