Lehrende: Prof. Dr. rer. nat. Marie-Christine Jakobs
Veranstaltungsart: Integrierte Veranstaltung
Orga-Einheit: FB20 Informatik
Anzeige im Stundenplan: ASV
Fach:
Anrechenbar für:
Semesterwochenstunden: 4
Unterrichtssprache: Englisch
Min. | Max. Teilnehmerzahl: - | -
Digitale Lehre: https://moodle.informatik.tu-darmstadt.de/course/view.php?id=815
Lehrinhalte: Die Veranstaltung befasst sich mit den Techniken zur automatischen Softwareverifikation und behandelt dabei folgende Themebereiche: - operationelle Semantik von sequentiellen Programmen - konfigurierbare Programmanalyse inklusive Konfiguration für Datenflussanalysen und Model Checking - counter-example guided abstraction refinement (CEGAR) - Bounded Model Checking - k-Induktion - kooperative Verifikation, insbesondere Conditional Model Checking - inkrementelle Verifikation - Nachprüfung von Verifikationsergebnissen (a la Proof-Carrying Code, Witness Validation) - Generierung von Testeingaben mittels Verifizierern
Voraussetzungen: Empfohlen: Informatikkenntnisse entsprechend der ersten vier Semester des Bachelorstudiengangs Informatik, insbesondere Kenntnisse aus der Vorlesung Aussagen und Prädikatenlogik oder Vergleichbares.
