Lehrende: Prof. Ph.D. Sebastian Faust
Veranstaltungsart: Integrierte Veranstaltung
Orga-Einheit: FB20 Informatik
Anzeige im Stundenplan: FormMeth SWentwurf
Fach:
Anrechenbar für:
Semesterwochenstunden: 3
Unterrichtssprache: Deutsch
Min. | Max. Teilnehmerzahl: - | -
Digitale Lehre: https://moodle.informatik.tu-darmstadt.de/course/view.php?id=1054
Lehrinhalte: - Modellierung nebenläufiger Software mit der Sprache ProMeLa - Formalisierung von Sicherheits- und Lebendigkeitseigenschaften mit temporaler Aussagenlogik - Theoretische Grundlagen von Modellprüfungsverfahren - Verifikation von ProMeLa Programmen mittels des Modellprüfers SPIN - Syntax, Semantik und Sequenzenkalkül für typisierte Logik erster Stufe - Grundlagen der kontraktbasierten Softwarespezifikationssprache JML - Dynamische Logik als eine Programmlogik erster Stufe - Formale Programmverifikation durch symbolische Ausführung und Invariantenschließen - Werkzeugunterstützte Verifikation von Java-Programen mit der KeY System
Literatur: Für den ersten Teil des Kurses: - Ben-Ari: Principles of the SPIN Model Checker, Springer - Holzmann: The SPIN Model Checker, Addison-Wesley Für den zweiten Teil des Kurses: - Beckert et al.: Verification of Object-Oriented Software, Springer Die Literaturempfehlungen werden kontinuierlich aktualisiert.
Voraussetzungen: Empfohlen: Programmierkenntnisse in Java und Vertrautheit mit Aussagenlogik wird erwartet. Empfohlen ist der Besuch der Vorlesung “Aussagen- und Prädikatenlogik”. Ansonsten genügt grundlegende mathematische Reife.
Formale Methoden im Softwareentwurf - Ü01
Prof. Ph.D. Sebastian Faust
Di, 13. Apr. 2021 [11:40]-Di, 13. Jul. 2021 [13:20]
Formale Methoden im Softwareentwurf - Ü02
Fr, 16. Apr. 2021 [08:55]-Fr, 16. Jul. 2021 [10:35]
Formale Methoden im Softwareentwurf - Ü03
Mi, 14. Apr. 2021 [13:30]-Mi, 14. Jul. 2021 [15:10]
Formale Methoden im Softwareentwurf - Ü04
Fr, 16. Apr. 2021 [11:40]-Fr, 16. Jul. 2021 [13:20]
Diese Kleingruppe wird aktuell angezeigt.