Verifikation von C-Programmen
Willkommen auf der Heimatseite der Lehrveranstaltung „Verifikation von C-Programmen 3“ im Wintersemester 2014/2015.
Inhalt
Verifikation bedeutet, dass wir beweisen wollen, dass ein Programm bestimmte Anforderungen erfüllt. Diese können funktional sein (Aussagen über die Funktionalität, bspw. dieses Programm berechnet die Länge einer Liste oder die konvexe Hülle einer Punktmenge), oder nicht-funktional (Aussagen über andere Eigenschaften, bspw. dieses Programm terminiert, wirft keine Aussagen, oder greift nicht auf undefinierte Adressen im Speicher zu).
In dieser Veranstaltung wollen wir am Beispiel einer realen Programmiersprache, nämlich C, Methodik und Grundlagen der Verifikation von Programmen darstellen.
Struktur
- Einführung in die Sprache:
- Wir lesen den Standard
- Einführung in Verifikation
- Was ist das?
- Standards, V-Modell, IEC 61508, DO178-B &c;
- V&V, Verifkationsaktivitäten
- Codierrichtlinien: eg. MISRA-C
- Umgang mit MISRA-C, Compliance Matrix etc.
- Statische Programmanalyse
- Grundlagen
- Werkzeuge
- Valgrind
- llvm -> scan-build
- gcc -> propolice
- Funktionale Verifkation
- Grundlagen
- Werkzeuge:
- Frama-C
- VCC