185.291 Formale Methoden der Informatik
Diese Lehrveranstaltung ist in allen zugeordneten Curricula Teil der STEOP.
Diese Lehrveranstaltung ist in mindestens einem zugeordneten Curriculum Teil der STEOP.

2023S, VU, 4.0h, 6.0EC
TUWEL

Merkmale

  • Semesterwochenstunden: 4.0
  • ECTS: 6.0
  • Typ: VU Vorlesung mit Übung
  • Format der Abhaltung: Präsenz

Lernergebnisse

Nach positiver Absolvierung der Lehrveranstaltung sind Studierende in der Lage...

  • grundlegende Methoden der Berechnungstheorie anzuwenden um z.B unentscheidbare Probleme zu identifizieren
  • fundamentale Methoden der Komplexitätstheorie auf neue Probleme anzuwenden, insb. um zu zeigen ob ein Problem polynomiell lösbar oder NP-schwer ist,
  • Probleme aus dem Bereich der formalen Methoden als Erfüllbarkeitsprobleme darzustellen, diese dann mit den entsprechenden Beweissystemen zu  lösen,  sowie die Korrektheit der benutzen Techniken und Reduktionen formal zu argumentieren,
  • partielle und vollständige Korrektheit von Softwaresystemen mittels deduktiver Verifikationsansätze basierend auf Hoare Logik und Prädikat-Transfomers formal zu zeigen. Die Studierenden sind außerdem imstande Programsemantiken zu formulieren sowie Programmeigenschaften algorithmisch zu zeigen,
  • die grundlegenden Techniken des Model Checking zu verstehen und anzuwenden: das Formulieren von Spezifikationen in Temporallogiken, das Schlussfolgern über Formeln in Temporallogiken, das Model Checking von Formeln auf Kripke Strukturen, das Anwenden von Techniken zur Reduktion des Zustandsraums, und der Einsatz von Bounded Model Checking für Verifikationsprobleme.

Inhalt der Lehrveranstaltung

Die Lehrveranstaltung behandelt vier Themenblöcke:

1. Grundzüge der Komplexitätstheorie: Problemreduktion, P versus NP, Unentscheidbarkeit;

2. Lösungsmethoden für das aussagenlogische Erfüllbarkeitsproblem (SAT):  Anwendungen in der Informatik;

3. Einführung in die formale Semantik von Programmiersprachen; formale Verifikation von Programmen;

4. Model checking mit Anwendungen in der Hard- und Softwareverifikation.

Didaktisches Vorgehen: Die Vorlesung wird von einer freiwilligen Übung begleitet, in der Aufgaben zu den vier Themenblöcken bearbeitet und zur Korrektur abgegeben werden können. Die Gesamtbeurteilung ergibt sich aus der abschließenden schriftlichen Prüfung.

Methoden

Die LVA is in 4 Themenblöcke unterteilt. Die LVA (und daher jeder Block) besteht aus einem Vorlesungs- und Vertiefungsteil.

Der Stoff der Lehrveranstaltung wird mittels Vorlesungsvideos präsentiert

Der Vertiefungsteil inkludiert pro Block drei zusätzliche Präsenz-Lehreinheiten, die der Diskussion und dem Lösen von Übungsaufgaben dienen. Studierende erhalten für jeden Themenblock eine Übungssammlung. Ihre Lösungen werden korrigiert um Feedback zu geben.

Drei weitere Vorlesungs-Einheiten dienen einer Wiederholung grundlegender Techniken zur Beweisführung.

 

 

Sollte CoVID-bedingt eine Umstellung von Präsenz auf Online notwendig werden, gibt es folgende Änderungen:

  • Prüfung: Wird verschoben oder online in Tuwel statt in Präsenz
  • Q+A Sessions via Zoom

 

 

Prüfungsmodus

Schriftlich

Weitere Informationen

Aufwandsabschätzung

  2 h Einleitung (erste Vorlesung)
60 h Vorlesung (20 Termine à 2h + 1h Vor-/Nachbereitung)
40 h Übungsbeispiele (4 Blätter mit je 10 Beispielen à 1h)
 16 h Diskussion der Übungsbeispiele (8 Termine à 2h)
30 h Testvorbereitung
2 h schriftlicher Test
-----------------------------------------------------------
150 h = 6 Ects

Vortragende Personen

Institut

LVA Termine

TagZeitDatumOrtBeschreibung
Mo.09:00 - 11:0006.03.2023 - 12.06.2023EI 8 Pötzl HS - QUER Q+A Sessions
Di.13:00 - 15:0007.03.2023 - 21.03.2023EI 2 Pichelmayer HS - ETIT Q+A Sessions
Di.13:00 - 15:0018.04.2023 - 20.06.2023EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mi.16:00 - 18:0031.05.2023FAV Hörsaal 1 Helmut Veith - INF FMI - Certora Talk by Prof. Mooly Sagiv
Formale Methoden der Informatik - Einzeltermine
TagDatumZeitOrtBeschreibung
Mo.06.03.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Di.07.03.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mo.13.03.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Di.14.03.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mo.20.03.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Di.21.03.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mo.27.03.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Mo.17.04.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Di.18.04.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mo.24.04.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Di.25.04.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Di.02.05.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mo.08.05.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Di.09.05.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mo.15.05.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Di.16.05.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mo.22.05.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions
Di.23.05.202313:00 - 15:00EI 2 Pichelmayer HS - ETIT Q+A Sessions
Mi.31.05.202316:00 - 18:00FAV Hörsaal 1 Helmut Veith - INF FMI - Certora Talk by Prof. Mooly Sagiv
Mo.05.06.202309:00 - 11:00EI 8 Pötzl HS - QUER Q+A Sessions

Leistungsnachweis

Die Gesamtbeurteilung erfolgt auf Basis einer schriftlichen Abschlussprüfung.

Prüfungen

TagZeitDatumOrtPrüfungsmodusAnmeldefristAnmeldungPrüfung
Mi.09:00 - 12:0026.06.2024Informatikhörsaal - ARCH-INF schriftlich03.06.2024 09:00 - 24.06.2024 23:59in TISSExam 4 WS
Di. - 21.01.2025schriftlich29.12.2024 00:00 - 17.01.2025 23:59in TISSExan 1 WS
Fr. - 21.03.2025schriftlich04.03.2025 00:00 - 17.03.2025 23:59in TISSExam 2 WS
Fr. - 23.05.2025schriftlich14.04.2025 09:00 - 16.05.2025 23:59in TISSExam 3 WS
Mi. - 25.06.2025schriftlich02.06.2025 09:00 - 23.06.2025 23:59in TISSExam 4 WS

LVA-Anmeldung

Von Bis Abmeldung bis
16.02.2023 00:00 26.03.2023 23:59 26.03.2023 23:59

Curricula

StudienkennzahlVerbindlichkeitSemesterAnm.Bed.Info
066 504 Masterstudium Embedded Systems Gebundenes Wahlfach
066 931 Logic and Computation Pflichtfach1. Semester
066 933 Information & Knowledge Management Pflichtfach
066 937 Software Engineering & Internet Computing Pflichtfach1. Semester
066 938 Technische Informatik Pflichtfach1. Semester
860 GW Gebundene Wahlfächer - Technische Mathematik Keine Angabe

Literatur

Folien und Übungsbeispiele siehe TUWEL Online-Kurs.

Weitere Informationen

Sprache

Englisch