Seminar 11 May 11:00, 2012
Model-checking quantifizierter Linearer Temporaler Logik über Pointerprogrammen
In der automatische Verifikation werden Implementationen und Algorithmen auf bestimmte Eigenschaften überprüft, etwa dass eine bestimmte fatale Konstellation (z.B. „alle Ampeln einer Kreuzung sind grün“) nie erreicht wird. Diese Eigenschaften müssen dabei formal spezifiziert werden, wofür insbesondere temporale Logiken verwendet werden.
Mit herkömmlichen temporalen Logiken ist es nun aber nicht möglich sowohl etwas über den Lauf eines Programmes, als auch das Verhalten von bestimmten Objekten während dieses Laufes auszusagen. Gerade das sind aber Aussagen, die man, im Bezug auf Pointerprogramme, d.h. Programme, die mit Pointern und Objekten auf einem Heap umgehen, gerne treffen möchte.
Wir werden uns daher damit beschäftigt, wie man die bekannte temporale Logik LTL um Objektquantoren erweitern kann, um damit Pointerprogramme zu verifizieren. Insbesondere werden wir einen Modelchecking-Algorithmus für die allgemeinste Erweiterung, einer Obermenge(!) von LTL, nämlich CTL*, um Objektquantoren, die wir Q*CTL* genannt haben, präsentieren.
