|
|
|
|
Beschreibung |
|
KursbeschreibungIn vielen Anwendungsfällen möchte man sicher sein, dass ein Programm korrekt ist, also die gewünschte Eigenschaft hat. Besonders wenn Fehler extrem teuer oder gar lebensbedrohlich sein können, ist die Risikobereitschaft beim Einsatz von Software naturgemäß gering. Testen ist für solch sicherheitskritische Software unzureichend, denn Tests können nur bestehende Fehler aufdecken, aber nicht die Fehlerfreiheit attestieren. Daher wäre es wünschenswert, ein allgemeines Verifikationsverfahren zu haben, um die Korrektheit eines Programms zu beweisen. Der Satz von Rice stellt hier allerdings eine natürliche Grenze dar: Das Verifikationsproblem ist im Allgemeinen unentscheidbar. In diesem Seminar werden wir verschiedene Techniken betrachten, die das Verifikationsproblem - jedenfalls in gewissen Fällen - lösen. Behandelt werden unter anderem die Themen Verhaltensäquivalenzen, Model Checking und Abstrakte Interpretation. |
|
|
