Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage (u.a.)
diese Konzepte auf Methoden zur Programmtransformation/optimierung zu übertragen und anzuwenden.
Gemeinsamkeiten, Analogien und Unterschiede zwischen Programmanalyse und Programmverifikation zu verstehen und herauszuarbeiten.
die Möglichkeiten und Grenzen automatischer und semi-automatischer Verfahren zur Programmanalyse, Programmverifikation und Programmtransformation/-optimierung im Spannungsfeld von Entscheidbarkeit, Skalierbarkeit, Wirksamkeit und Nützlichkeit zu erkennen, einzuschätzen und zu bewerten.
Die Vorlesung beschäftigt sich mit Konzepten und Prinzipiengrundlegender und fortgeschrittener Verfahren zur Analyse undVerifikation von Softwaresystemen. Im Mittelpunkt stehen dabei dieKonzepte von Korrektheit, Vollständigkeit und Optimalität in Analyse,Verifikation und Transformation. Die Vorlesung spannt dabei den Bogenvon Hoarescher Logik über Programm- und Datenflussanalyse zurTheorie abstrakter Interpretation und Modellprüfung. IllustrierendeTransformationen werden dabei besonders dem Bereich optimierender undverifizierender Übersetzung entnommen. Anhand regelmäßig gestellterÜbungsaufgaben werden die in der Vorlesung behandelten Themen anmaßgeschneiderten Aufgabenstellungen erprobt und angewendet.
Teil I: Motivation
Teil II: Analyse und Verifikation
Teil III: Transformation und Optimalität
Teil IV: Abstrakte Interpretation und Modellprüfung
Teil V: Abschluss und Ausblick
Literaturverzeichnis
Anhang
Ausgewählte Leseempfehlungen
Abhaltemodus: Online
Aufgrund geltender COVID-19 Beschränkungen und Weisungen von Rektorat und Studiendekanat vom 26.01.2021 und 30.01.2021 findet die Lehrveranstaltung 185.276 Analyse und Verifikation im SS 2021 ausschließlich online statt. Die Vorteile der Unmittelbarkeit von Präsenzveranstaltungen sollen dabei möglichst umfassend erhalten bleiben. Die Veranstaltung findet deshalb in Form von Echtzeitvideokonferenzen statt.
Aufteilung der ECTS-Punkte:
Der Lehrveranstaltung sind 3.0 ECTS-Punkte zugeordnet. Dieseentsprechen einem durchschnittlichen Lernaufwand von 75Stunden. Dieser durchschnittliche Lernaufwand verteilt sich infolgender Weise auf die einzelnen Lernaktivitäten der Lehrveranstaltung(die Angaben Teil I bis Teil V beziehen sich auf die entsprechenden Teileder Lehrveranstaltungsunterlagen):
Die Lehrveranstaltung beginnt mit Vorbesprechung und erster Vorlesung am Mittwoch, den 03.03.2021, 16:15 Uhr bis 18:00 Uhr (einschließlich einer 15min Pause) via Zoom. Der Zoom-Link ist am 01.03.2021 per TISS-Nachricht ausgesandt worden; er findet sich auch auf dem Lehrveranstaltungsnachrichtenbrett in TISS und im zugehörigen TUWEL-Kurs.
Weitere beurteilte Leistungsnachweise gibt es nicht.
Erforderliche technische Voraussetzungen: Stabiler Internetanschluss, internetfähiges Endgerät mit Audio/Video-Empfang und Übertragung.
Grundlegende Kenntnisse in Theoretischer Informatik und Programmierungwerden vorausgesetzt. Kenntnisse im Übersetzerbau sind nützlich, etwaaus den Lehrveranstaltungen 185.A48 VU 4.0h "Übersetzerbau" oder185.A04 VU 2.0 "Optimierende Compiler", aber nicht zwingenderforderlich.
Die Vorlesung ergänzt die Lehrveranstaltungen 185.A04 "OptimierendeCompiler" und 185.A56 "Semantik von Programmiersprachen". Sieempfiehlt sich deshalb inbesondere für Studierende, die im Bereich vonProgrammiersprachen und Übersetzerbau einen besonderen Schwerpunktsetzen, eine Seminararbeit, ein Praktikum oder ihre Diplomarbeitanfertigen möchten.