Vorlesungen im Sommersemester 2023

Bitte beachten Sie:
Diese Auflistung bezieht sich auf des Sommersemester 2023. Ein Update für das Sommersemester 2024 erfolgt noch!

Im Sommersemester finden am KASTEL-Institut eine Reihe von Vorlesungen zu verschiedenen Themen aus dem Gebiet der Formalen Methoden statt. Jede Veranstaltung hat ihren besonderen Schwerpunkt und diese Seite will Ihnen einen Überblick über das Angebot geben.

Das Stammmodul Formale Systeme liefert eine gute Basis für alle Veranstaltungen.

Im Institutsseminar gibt es auch eine Reihe an interessanten Vorträgen rund um formale Methoden.

Formale Systeme 2 – Anwendung

Umfang:3 SWS / x Leistungspunkte
Vertiefungsfächer:Theoretische Grundlagen und Softwaretechnik und Übersetzerbau
Zeit:Dienstags 11:30-13:00 und Freitags 11:30-13:00
Ort:SR 236, Geb. 50.34
Bemerkung:Nur jedes zweite Jahr, im Wechsel mit Formale Systeme 2 - Theorie
> > > > Link zur Vorlesung < < < <

Methoden für die formale Spezifikation und Verifikation - zumeist auf der Basis von Logik und Deduktion - haben einen hohen Entwicklungsstand erreicht. Es ist zu erwarten, dass sie zukünftig traditionelle Softwareentwicklungsmethoden ergänzen und teilweise ersetzen werden. Formale Methoden haben den Bereich akademischer Fallstudien hinter sich gelassen, und die Softwareindustrie zeigt ernsthaftes Interesse. Nahezu sämtliche formale Spezifikations- und Verifikationsverfahren haben zwar die gleichen theoretisch-logischen Grundlagen, wie man sie etwa in der Vorlesung "Formale Systeme" kennenlernt. Zum erfolgreichen praktischen Einsatz müssen die Verfahren aber auf die jeweiligen Anwendungen und deren charakteristischen Eigenschaften abgestimmt sein. An die Anwendung angepasst sein müssen dabei sowohl die zur Spezifikation verwendeten Sprachen als auch die zur Verifikation verwendeten Kalküle. Auch stellt sich bei der praktischen Anwendung die Frage nach der Skalierbarkeit, Effizienz und Benutzbarkeit (Usability) der Verfahren und Werkzeuge.

Formale Systeme 2 – Theorie

findet wieder im Sommersemester 2024 statt. (Im Wechsel mit Formale Systeme 2 – Anwendung)

Timed Systems

Umfang:2 SWS / 3 Leistungspunkte
Vertiefungsfächer:Theoretische Grundlagen und Softwaretechnik und Übersetzerbau
Zeit:Donnerstags 11:30-13:00
Ort:SR 301, Geb. 50.34
Bemerkung:Vermutl. 1x jährlich im Sommersemester, Sprache deutsch/englisch
> > > > Link zur Vorlesung < < < <

Viele der (eingebetteten) Software-Systeme mit denen wir im Alltag konfrontiert sind, haben zeitkritische Funktionalitäten. Beispielsweise sollte ein Airbag bei einem Unfall innerhalb einer bestimmten, sehr kurzen, Zeitspanne aktiviert werden. Ebenso erwarten wir von den diversen Apps auf unseren Smartphones schnelle Antwortzeiten, um sie komfortabel und zielbringend zu nutzen. Bei der Modellierung von Software-Systemen ist somit „Zeit“ ein entscheidender Faktor. In dieser Vorlesung werden verschiedenen Mechanismen beschrieben sogenannte Realzeitsysteme zu formalisieren. Neben der Modellierung steht auch die Analyse der Systeme im Fokus der Vorlesung. Es werden insbesondere folgende Themen behandelt:

  • Timed Automata (eine Erweiterung endlicher Automaten um Zeit)
  • Model-Checking von Timed Automata mit Hilfe von UPPAAL
  • Timed Games (Zwei Spieler versuchen eigene Ziele in einem zeitkritischen Spiel zu erreichen)
  • Interval Temporal Logic (eine Logik die über Zeitintervalle spricht)
  • Erweiterungen und Anwendungen von Timed Systems

Die wöchentliche Vorlesung besteht sowohl aus theoretischen als auch angewandten Anteilen. Die angewandten Anteile bestehen aus freiwilligen Übungsaufgaben, die in der Vorlesung besprochen werden.

Constructive Logic

Umfang:3+1 SWS / 5 Leistungspunkte
Vertiefungsfächer:Theoretische Grundlagen und Softwaretechnik und Übersetzerbau
Zeit: Montags 11:30-13:00, Donnerstags 09:45-11:15
Ort: SR 131, Geb. 50.34
Bemerkungen:Sprache englisch/deutsch
> > > > Link zur Vorlesung < < < <

This course provides a thorough introduction to modern constructive logic, its roots in philosophy, its numerous applications in computer science, and its mathematical properties. The core topics of this course are intuitionistic logic, natural deduction, Curry-Howard isomorphism, propositions as types, proofs as programs, formulas as programs, functional programming, logic programming, Heyting arithmetic and primitive recursion, cut elimination, connections between classical and constructive logic, inductive definitions, sequent calculus, and decidable classes. Advanced topics may include type theory, proof search, linear logic, temporal logic, modal logic.

Seminare

Neben den Vorlesungen gibt es auch Seminare, deren Inhalte sich (u.a.) mit der Anwendung Formaler Methoden in der Software-Entwicklung auseinandersetzen.

Softwarequalitätssicherung und Softwaretest

Die Bereitstellung qualitativ hochwertiger Software ist ein integraler Bestandteil des Software-Entwicklungsprozesses. So können Software-Bugs unter Umständen Millionen oder im schlimmsten Falls sogar Menschenleben kosten. Dadurch, dass die Technologien, um Software zu entwickeln, sich stetig weiterentwickeln, steht die Softwarequalitätssicherung stets vor der Herausforderung, die Qualität der immer komplexer werdenden Software zu gewährleisten.

Am Lehrstuhl "Test, Validierung und Analyse Software-intensiver Systeme" (Prof. Schaefer und Mitarbeiter:innen)

> > > > Link zum Seminar < < < <

Anwendung Formaler Verifikation: Von der Theorie zur Anwendung

In diesem Seminar werden verschiedene formale Techniken vorgestellt, die dazu beitragen, Programme auf ihre Korrektheit überprüfen zu können. Einige Techniken stellen neue vielversprechende Ansätze vor, andere zeigen auf wie durch geschickten Einsatz und Kombination von Heuristiken existierende Ansätze um Größenordnungen leistungsfähiger gemacht werden können. Die vorgestellten Ansätze helfen praxisnah, Probleme in Software zu entdecken, zu vermeiden oder zu verhindern.

Am Lehrstuhl "Anwendungsorientierte Formale Verifikation" (Prof. Beckert und Mitarbeiter:innen)

> > > > Link zum Seminar < < < <

Praktika

Fortgeschrittene Software-Entwicklungswerkzeuge

Die Anforderungen an moderne Software werden immer höher und komplexer. Damit einhergehend werden auch immer neue Techniken zur Entwicklung von Software vorgestellt, die diese Anforderungen erfüllen sollen. Oftmals müssen dafür in der Forschung neue Entwicklungsumgebungen und Werkzeuge implementiert werden, die diese fortgeschrittenen Entwicklungstechniken unterstützen.

In diesem Modul benutzen und erweitern die Teilnehmenden fortgeschrittene Software-Entwicklungswerkzeuge aus der Praxis und Forschung. Dadurch soll entweder die Funktionalität erweitert oder das Werkzeug im Bereich der nicht-funktionalen Eigenschaften verbessert werden.

Am Lehrstuhl "Test, Validierung und Analyse Software-intensiver Systeme" (Prof. Schaefer und Mitarbeiter:innen)

> > > > Link zum Praktikum < < < <

Forschungspraktikum im Rahmen der Vorlesung Formale Systeme 2

In diesem Semester bieten wir neben der Vorlesung ein optionales begleitendes Forschungspraktikum im Umfang von insgesamt fünf Leistpungspunkten (LP) (davon zwei Schlüsselqualifikation (SQ)) an. Hierbei handelt es sich um ein Projektpraktikum, in dem über das ganze Semester an einem Thema gearbeitet wird (und nicht an verschiedenen Aufgabenblättern). Die Bearbeitung aktueller Forschungsthemen erfordert hierbei ein größeres Maß an Eigeninitiative als dies bei im Vorhinein festgelegten Praktika der Fall ist. Die Fortschritte werden dabei regelmäßig mit einem bzw. einer betreuenden Mitarbeitenden der Forschungsgruppe diskutiert.

Am Lehrstuhl "Anwendungsorientierte Formale Verifikation" (Prof. Beckert und Mitarbeiter:innen)

> > > > Link zum Praktikum < < < <