Entwicklung korrekter Systeme

Programmverifikation

Auf dieser Seite

 
 

zum Seitenanfang

Termine 


Programmverifikation (4 VL,2 Ü)            

      Stammvorlesung
        Dienstag 10-12, HS F             Olderog
        Mittwoch 8-10 HS F

      Übungen                        
        Dienstag 14-16, A5 1-160         Wehrheim

 

zum Seitenanfang

Inhalt

Programmverifikation ist ein systematischer Ansatz, die Fehlerfreiheit von Programmen zu zeigen. Dazu wird bewiesen, daß ein vorgegebenes Programm bestimmte wünschenswerte Eigenschaften besitzt.

Bei sequentiellen Programmen geht es dabei vor allem um partielle Korrektheit, Terminierung und Abwesenheit von Laufzeitfehlern. Bei parallelen und verteilten Programmen sind zusätzliche Eigenschaften wichtig:
Interferenz-Freiheit, Deadlock-Freiheit und faires Ablaufverhalten.

In der Vorlesung geht es vornehmlich um die Verifikation paralleler und verteilter Programme. Dazu werden klassische Methoden der Hoareschen Logik mit neuen Techniken der Programmtransformation kombiniert. Als Vorbereitung werden aber auch sequentielle Programme, insbesondere solche mit nichtdeterministischen Konstrukten, behandelt.

 

zum Seitenanfang

Literatur

K.R. Apt, E.-R. Olderog, Programmverifikation, Springer-Verlag, 1994.

Errata-Liste bzw.
Errata-Liste mit Tippfehlern

 

zum Seitenanfang

Übungsaufgaben

Sie haben hier die Möglichkeit, die aktuellen Übungsblätter zu dieser Lehrveranstaltung im Postscript- oder DVI-Format abzurufen. Wir bitten Sie jedoch im Interesse aller, die Übungsblätter nicht gedankenlos auszudrucken, insbesondere nicht auf den Laserdruckern der ARBI. Fotokopien sind unter Berücksichtigung aller Kosten in der Regel günstiger als Laserdrucke!

Dieses Angebot richtet sich hauptsächlich an diejenigen, die auf anderem Wege kein Exemplar der Übungsblätter erhalten konnten.