Programmverifikation

Auf dieser Seite

• Termine
• Inhalt
• Literatur

 
 

Termine

Programmverifikation (VL,Ü)            
 
        Stammvorlesung
        Dienstag   8.25-9.55  HS F         Olderog
        Donnerstag 8.25-9.55  HS F
 
        Übungen                         
        Montag 8-10,  A4 3-307            Brückner
        Montag 10-12, A4 2-221             Dierks
 

 

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.

 

Literatur

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

Errata-Liste bzw.
Errata-Liste mit Tippfehlern