| Veranstalter: |
Prof. Dr. Falk Howar |
|---|---|
| Veranstaltungsnummer: | 042359 |
| Typ: | Vertiefungsmodul in den Masterstudiengängen Informatik und Angewandte Informatik Forschungsbereich: Software, Sicherheit und Verifikation |
| Modulnummer: | folgt |
| SWS: | 2 SWS Vorlesung 1 SWS Übung |
| Ort: | Otto-Hahn-Str. 12, 2.063 |
| Zeit: | 10:15–12:00 Uhr |
| Beginn: | Mittwoch, 12.10.2022 |
| Anmeldung: | via LSF, |
| Vorlesung: |
Mittwoch, 10:15–12:00, OH12 2.063 |
wöchentlich | |
|---|---|---|---|
| Übung: |
Donnerstag, 14:15-16:00, OH12 2.063 |
wöchentlich | |
Die Vorlesung vermittelt Konzepte im Bereich der automatisierten formalen Verifikation von Software.
Der Fokus der Veranstaltung liegt dabei insbesondere auf Verfahren, die das Verifikationsproblem auf ein logisches Erfüllbarkeitsproblem oder in eine Automaten-basierte Repräsentation abbilden. Als Grundlage für die Automatisierung der betrachteten Verifikationsverfahren werden die Mechanisierung formaler Logik diskutiert und entsprechende algorithmische Resultate studiert. Im Bereich der Verifikation von Programmen werden deduktive und induktive Verfahren verglichen. Ausgehend von klassischer Hoare-Logik und einfacher Suche werden z.B. Verfahren auf betrachtet, die induktive Invarianten bei der Verifikation generieren. Im Bereich der Verifikation von Software Komponenten werden Verfahren diskutiert, die formale Verhaltensmodelle aus Implementierungen generieren, sowie Verfahren, die logische Eigenschaften auf Verhaltensmodellen (z.B. Automaten) prüfen.
In der Übung soll neben der Anwendung der algorithmischen Ergebnisse auch die Benutzung von Werkzeugen, die die vorgestellten Konzepte implementieren, trainiert werden.
Im Zusammenhang mit den in der Vorlesung behandelten Themen werden auch Abschlussarbeiten betreut.
Entsprechend einem Beschluss des Fakultätsrates, dass bei offiziellen Emails der Fakultät entweder die Uni-Mail-Adresse des ITMC oder die Postamt-Adresse der IRB verwendet werden sollen, möchte ich darauf aufmerksam machen, dass ab sofort nur noch diese Adressen verwenden werden. Bitte aktivieren Sie diese umgehend und schicken Sie nur noch eine Mail mit der richtigen Adresse als Absender.