Aktuelle Themen im logikbasierten Software Engineering

Description

Since the beginning of the 21st century, formal proof methods have become standard in industrial hardware verification, particularly in CPU verification (Intel, AMD). During the past decade, the proof assistant technology has matured enough to also enable formal certification of substantial software systems. Two major success stories are the seL4 operating system microkernel and the CompCert optimising C compiler. Recently, deductive program verification has attracted increasing attention in the software industry (Microsoft, Amazon, Facebook, Galois). To quote Nikhil Swamy from Microsoft Research:

"Today, what seemed impossible just a few years ago is becoming a reality. We can, in certain domains, produce fully verified software at a nontrivial scale and with runtime performance that meets or exceeds the best unverified software."

This lecture is about writing functional programs in a dependently typed language and proving them correct.

Coq - the 2013 ACM Software System Award winner - is an interactive proof assistant for the development of formally certified software and mathematical theories. Its underlying theory is the Calculus of Inductive Constructions - a variant of dependent type theory with inductive types. The lecture covers programming and proving in Coq, dependent type theory, and applications to program verification. There is overlap with LMSE 1 & 2, but no familiarity with type theory is necessary. ATLSE focuses on dependently typed functional programming, verification of functional programs, proof automation, theoretical foundations of inductive and dependent types.

Prerequisites

Some experience with functional programming and formal logic. You should understand mathematical induction. If you liked the logic and/or the functional programming bachelor courses then this lecture is for you. If you're interested in formal methods and security then this may also be for you. The lecture is self-contained: knowledge of type theory or previous participation in LMSE are not necessary.

Supplementary Materials

• Certified Programming with Dependent Types and Formal Reasoning About Programs by Adam Chlipala
• Software Foundations by Benjamin C. Pierce et. al.
• Interactive Theorem Proving and Program Development by Yves Bertot and Pierre Casteran
• Inductive definitions in the system Coq: rules and properties by Christine Paulin-Mohring
• History of Interactive Theorem Proving by John Harrison, Josef Urban and Freek Wiedijk

Description

Since the beginning of the 21st century, formal proof methods have become standard in industrial hardware verification, particularly in CPU verification (Intel, AMD). During the past decade, the proof assistant technology has matured enough to also enable formal certification of substantial software systems. Two major success stories are the seL4 operating system microkernel and the CompCert optimising C compiler. Recently, deductive program verification has attracted increasing attention in the software industry (Microsoft, Amazon, Facebook, Galois). To quote Nikhil Swamy from Microsoft Research:

"Today, what seemed impossible just a few years ago is becoming a reality. We can, in certain domains, produce fully verified software at a nontrivial scale and with runtime performance that meets or exceeds the best unverified software."

This lecture is about writing functional programs in a dependently typed language and proving them correct.

Coq - the 2013 ACM Software System Award winner - is an interactive proof assistant for the development of formally certified software and mathematical theories. Its underlying theory is the Calculus of Inductive Constructions - a variant of dependent type theory with inductive types. The lecture covers programming and proving in Coq, dependent type theory, and applications to program verification. There is overlap with LMSE 1 & 2, but no familiarity with type theory is necessary. ATLSE focuses on the following aspects:

• dependently typed functional programming
• verification of functional programs
• proof automation
• theory of inductive types

Prerequisites

Some experience with functional programming and formal logic. You should understand mathematical induction. If you liked the logic and/or the functional programming bachelor courses then this lecture is for you. If you're interested in formal methods and security then this may also be for you. The lecture is self-contained: knowledge of type theory or previous participation in LMSE are not necessary.

Supplementary Materials

• Certified Programming with Dependent Types and Formal Reasoning About Programs by Adam Chlipala
• Software Foundations by Benjamin C. Pierce et. al.
• Interactive Theorem Proving and Program Development by Yves Bertot and Pierre Casteran
• Inductive definitions in the system Coq: rules and properties by Christine Paulin-Mohring
• History of Interactive Theorem Proving by John Harrison, Josef Urban and Freek Wiedijk

Proseminar - Lösungsansätze für das Expression Problem

Neuigkeiten und Ankündigungen

• 17.03.2024: Termine und Moodle angelegt, Studierende per Mail eingeladen/informiert
• 16.12.2024: Seite mit Informationen angelegt.

Beschreibung

In der Theorie der Programmiersprachen gibt es ein altbekanntes Problem:

Gegeben einen Datentypen und Funktionen über diesem Typen. Erweitere den Datentypen und füge weitere Funktionen hinzu, ohne den bestehenden Code neu kompilieren zu müssen. Die statische Typsicherheit muss ebenfalls erhalten bleiben.

Betrachten wir zur Verdeutlichung das Problem am Beispiel von Objekt-orientierten und funktionalen Programmiersprachen. In beiden Fällen vereinfachen wir die Konzepte der Sprachparadigmen soweit, dass das Problem deutlich wird.

Bei Objekt-orientierten Sprachen nennen wir Datentypen Klassen und Funktionen Methoden, welche in der Klasse selbst definiert werden. Es ist einfach eine Klasse durch Unterklassen zu erweitern, ohne die bestehende Klassendefinition zu ändern. Allerdings bedingt das Hinzufügen einer weiteren Methode, dass die ursprüngliche Klassendefinition und die Definitionen aller Unterklassen erweitert und damit der bestehende Code neu kompiliert werden muss.

Komplementär dazu verhalten sich funktionale Sprachen. Hier werden Datentypen über Konstruktoren und Funktionen als Fallunterscheidungen auf diesen Konstruktoren definiert. Man kann einfach weitere Funktionen hinzufügen, ohne den Datentyp ändern zu müssen. Wenn man einen Datentyp jedoch um einen neuen Konstruktor erweitert, dann müssen alle Fallunterscheidungen in den Funktionsdefinitionen erweitert werden und damit ebenfalls der bestehende Code neu kompiliert werden.

Dieses Problem tritt bei allen Programmiersprachen auf und wurde bereits 1975 von John C. Reynolds untersucht. 1998 benennt Philip Wadler das Problem mit dem Namen "Expression Problem".

Es gibt viele unterschiedliche Lösungsansätze zum Expression Problem und es wird auch heute noch aktiv daran geforscht. Einige dieser Lösungsansätze müssen bereits beim Entwurf einer Programmiersprache umgesetzt werden, während andere Lösungsansätze probieren Design Patterns zu finden, die in bereits existierenden Sprachen umgesetzt werden können.

Daher ist das Expression Problem nicht nur ein grundlegendes Problem des Entwurfs von Programmiersprachen, sondern auch des Software Developments.

Wir werden in diesem Proseminar die unterschiedlichen Lösungsansätze für das Expression Problem behandeln.

Leistung

• Benoteter Vortrag (20 Minuten Vortragszeit + 5 Minuten Rückfragen)
• Schriftliche, benotete Ausarbeitung
• Teilnahme an den Vorträgen von anderen Teilnehmenden

Die Abschlussnote bewertet den Vortrag und die Ausarbeitung.

Feedback

Wir haben großes Interesse an veranstaltungsbegleitendem Feedback, um auf Änderungswünsche eingehen zu können. Bitte äußern Sie entsprechende Hinweise im persönlichen Gespräch nach den Veranstaltungen oder per Mail.

Vielen Dank!

Aktuelles

• 17.03.25: Webseite und Moodle angelegt

Beschreibung

Die Lehrveranstaltung behandelt Konzepte und Anwendungen funktionaler Programmierung anhand der funktionalen Programmiersprache Haskell. Funktionale Programme unterscheiden sich zunächst stark von dem einer objektorientierten, imperativen und zustandsorientierten Sprache wie Java. Sie erlauben aber oft problemnahere und flexiblere Lösungen, die leicht an neue Anforderungen, modifizierte Datenstrukturen, etc. anpassbar sind.
Auf Basis des Buchs "Haskell - Eine Einführung für Objektorientierte" von Prof. Dr. Ernst-Erich Doberkat wird es eine Spracheinführung in Haskell geben. Das Buch ist über die Universitätsbibliothek ausleihbar und als Ebook zu haben.
Neben der Spracheinführung in Haskell wird die Lehrveranstaltung auch grundlegende theoretische Konzepte von (funktionalen) Programmiersprachen betrachten. Hierzu werden unter anderem ausgewählte Themen des Lambda-Kalküls, sowie der Typ- und Kategorientheorie betrachtet.
Abschließend wird es auf Basis der gewonnen Kenntnisse einen Überblick über andere funktionalen Sprachen wie z.B. Coq oder Scala und deren Unterschiede zu Haskell geben.

Vorlesungsmaterial

Vorlesungsmaterialien werden semesterbegleitend im Moodle bereitgestellt.

Die Vorlesung nutzt zur Spracheinführung u.a. die Folien von Prof. Dr. Ernst-Erich Doberkat aus dem WS12/13.

Übung

• Die Übung zu FuPro ist eine Präsenzübung.
• Die Übung dient der Verstetigung des Vorlesungsinhalts sowie der praktischen Anwendung der erlangten Kenntnisse.

Anmeldung

Es gibt keine Anmeldung für die Übungen. Sie können einfach die Übungstermine besuchen, die Ihnen zeitlich passen.

Übungsgruppen

Übungsaufgaben

Begleitend zur Vorlesung werden wöchentlich Übungsaufgaben im Moodle veröffentlicht und in der darauf folgenden Woche in den Übungsgruppen besprochen.

Es wird dringend empfohlen diese Übungsaufgaben eigenständig zu bearbeiten und eventuell aufkommende Fragen oder Probleme in den Übungsgruppen anzusprechen.

Es wird keine wöchentlichen Abgaben geben.

Studienleistung

Das Erlangen der Studienleistung ist Voraussetzung für die Teilnahme an der abschließenden Klausur.
Die Kriterien der Studienleistung sind wie folgt:

• Erfolgreiche Teilnahme am Midterm-Test. Dieser findet am Freitag, den 13.06.2025 während der Vorlesungszeit statt. 

Tutorium

Während der Vorlesungszeit wird zusätzlich zu den Übungen ein Tutorium angeboten.

Das Tutorium dient der

• Erläuterung zentraler Begriffe anhand konkreter Beispiele
• Vorstellung von Lösungen alter Übungs- und Klausuraufgaben
• Vermittlung von Techniken zur Lösung von Aufgaben
• Diskussion häufiger Fehler.

Das Tutorium findet ab dem 23.04.2024 Mittwochs von 14h-16h im Raum OH12/E.003 statt.

Klausuren

Die Klausurtermine sind voraussichtlich:

• Mittwoch, der 06.08.2025, von 15:30h-17:30h im Audimax
• Dienstag, der 16.09.2025, von 14:00h-16:00h im Audimax

Informationen zur Lehre im Sommersemester 2025

• Übungsabgaben werden digital über das Moodle durchgeführt. Fragen werden über das Moodle Forum beantwortet.
• Die Veranstaltung ist identisch mit der ehemaligen Veranstaltung "elektronische Geschäftsprozesse" (eGP). Studierende der Dienstleistungsinformatik können dieses Modul belegen, sofern sie das Modul eGP noch nicht bestanden haben. Nicht bestandende Versuche werden aus dem Modul eGP übernommen!

Klausurtermine

Werden noch bekannt gegeben.

Beschreibung

Anwendung von nebenläufigen Prozessen reichen von Abläufen inerhalb eines Unternehmens, über parallele Prozesse in einem Computersystem bis zu verteilten Systemen, in denen mehrere Anwendungen synchronisiert miteinander Kommunizieren müssen.

Die Lehrveranstaltung vermittelt Konzepte und Techniken zur Modellierung, Analyse und Implementierung von verteilten nebenläufigen Prozessen. Dazu wird Prozesstheorie anhand formaler Modelle betrachtet, und Programmiermodelle und Programmiersprachen für nebenläufige verteilte Prozesse werden eingeführt.  Diese werden sowohl in Theorie - anhand verschiedener Formalismen - als auch in Praxis - anhand des Frameworks Akka - vorgestellt.

Voraussetzungen

• Erfolgreicher Abschluss von DAP 1

Vorlesungsfolien

• Die Vorlesungsfolien sind aus dem Moodle-Arbeitsraum der Vorlesung abrufbar. Sie werden semesterbegleitend fortlaufend bereitgestellt.
• Im Anschluss daran kann es natürlich noch zu kleineren Änderungen kommen (z.B. das Hinzufügen der Antwort-Folien zu den während einer Vorlesung gestellten Diskussionfragen im Anschluss an eine Vorlesung).

Übung

Zeit und Ort

• Donnerstag 10:15-11:45, OH12, 1.056
• Donnerstag 14:14-15:45, OH12, 1.056

Konzept

• Die Übung dient der Verstetigung des Vorlesungsinhalts sowie der praktischen Anwendung der erlangten Kenntnisse über die unterliegenden Grundlagen elektronischer Geschäftsprozesse.
• Insbesondere Konzepte und Methodiken der Prozessmodellierung werden vertieft. Dafür werden in den Übungen die in der Vorlesung vorgestellten Modellierungsmethodiken aufgearbeitet sowie ihre Vorzüge und Grenzen sowohl auf theoretischer Ebene als auch in Form praktischer Beispiele gegenübergestellt.

Ablauf

• Bereitstellung und Abgabe der Übungszettel erfolgt über den zur Vorlesung gehörenden Moodle-Arbeitsraum.
• Die Bearbeitung der Übungszettel ist freiwillig und können über das Moodle abgegeben werden.
• Im Verlauf der Veranstaltung wird es zwei Projekte geben, die beide innerhalb von zwei Wochen bearbeitet werden müssen.

Studienleistung

• Das erfolgreiche Bearbeiten beider Projekte ist erforderlich für die Studienleistung.
• Die Projekte können in Gruppen von bis zu vier Studierenden abgegeben werden.
• Die Abgabe findet über das Moodle statt.

Einordnung

Bachelor Informatik:

Wahlmodul in den Bachelor-Studiengängen Informatik und Angewandte Informatik

Angewandte Informatik:

Pflichtmodul im Bachelorstudiengang Angewandte Informatik, Anwendungsfach Dienstleistungsinformatik / Wahlmodul in den Bachelor-Studiengängen Informatik und Angewandte Informatik

Proseminar - Perlen der funktionalen Programmierung

Veranstalter: Dr. Andrej Dudenhefner
Typ: Proseminar
Modulnummer: INF-BSc-110
Termine: wird bekanntgegeben
Ausarbeitung: 5 Seiten als PDF, Deutsch oder Englisch, EasyChair Format

Aktuelles

Beschreibung

In diesem Proseminar wollen wir uns mit "Perlen" der funktionalen Programmierung befassen:

• elegante Algorithmen
• effiziente Datenstrukturen
• Domain-spezifische Programmbibliotheken (z.B. für Parsing)
• Herleitung von (effizienten) Programmen aus korrekten, aber ineffizienten Beschreibungen

Neben den fachlichen Aspekten sollen das Lesen, Zusammenfassen und die Präsentation von Forschungsergebnissen erlernt werden.

Die Vortragsthemen des Proseminars basieren größtenteils auf Forschungsartikeln, die als "Functional Pearls" in der Zeitschrift Journal of Functional Programming oder einer der großen Konferenzen im Bereich Programmiersprachen erschienen sind.

Einige dieser Arbeiten benutzen die Programmiersprache Haskell. Daher werden wir uns in den ersten Treffen etwas näher mit den Besonderheiten von Haskell beschäftigen:
bedarfsgesteuerte Auswertung und "unendliche" Datenstrukturen, Haskell Typsystem, Typklassen und monadische Typen.

Leistung

• Benoteter Vortrag (20 Minuten Vortragszeit + 5 Minuten Rückfragen)
• Schriftliche, benotete Ausarbeitung (5 Seiten)
• Teilnahme an den Vorträgen von anderen Teilnehmenden

Die Abschlussnote bewertet die Qualität der Diskussionsbeiträge, den Vortrag und die Ausarbeitung.

Präsentationstechniken

Das Element Präsentationstechniken (1 CP) des Moduls Proseminar (INF-BSc-110) findet in Präsenz statt und umfasst folgende Termine. 

Zeit: wird bekanntgegeben
Ort: wird bekanntgegeben
Termine: wird bekanntgegeben
Beispiel: Eigenheiten der Kochschen Schneeflocke, LaTeX Quellcode

Themenliste

1. A Play on Regular Expressions
2. A Poor Man's Concurrency Monad
3. A Pretty But Not Greedy Printer
4. A Program to Solve Sudoku
5. A Short Cut to Deforestation
6. All Sorts of Permutations
7. Composing Fractals
8. Data Types a la Carte
9. Enumerating the Rationals
10. Every Bit Counts
11. Explaining Binomial Heaps
12. Fun with Semirings
13. Inverting the Burrows–Wheeler Transform
14. Lazy Wheel Sieves and Spirals of Primes
15. Monadic Parsing in Haskell
16. Parsing Permutation Phrases
17. Pickler Combinators
18. The Genuine Sieve of Eratosthenes
19. Two Can Keep a Secret If One of Them Uses Haskell
20. Typed quote_antiquote or Compile-time Parsing
21. I am not a Number - I am a Free Variable
22. HasChor Functional Choreographic Programming for All
23. On Generating Unique Names
24. Implicit Configurations - or Type Classes Reflect the Values of Types
25. Streams and Unique Fixed Points

Alternativ zu den oben genannten Themen kann (nach Absprache) eine Veröffentlichung der Zeitschrift Journal of Functional Programming im Bereich Functional Pearls behandelt werden.

FAQ

• Muss das gesamte Papier vorgestellt werden?
  • Nein. Eine Kompetenz des Proseminars ist die passende Auswahl der relevanten Materie für die gegebene Vortragslänge.
• Muss es einen Eigenanteil geben?
  • Ja. Es muss dem Betreuer deutlich werden, dass mit der Materie interagiert wurde.
    Am effektivsten sind eigene Beispiele, die nicht im Originalwerk enthalten sind.
• ​​​​​​Müssen noch andere Papiere eingebunden werden?
  • Ja. Der vorgestellte Inhalt soll kurz in den wissenschaftlichen Kontext eingeordnet werden.
    Oftmals reicht dazu die im Originalwerk referenzierte Literatur.
    Bei einer älteren Arbeit wäre eine Literaturrecherche sinnvoll.
• Dürfen nach der Abgabe des Folienentwurfs noch kleine Änderungen gemacht werden?
  • ​​​​​​​Ja. Für die Benotung zählt die Version, die beim Vortrag verwendet wird.
• Muss jedes Codeschnipsel einzeln referenziert werden?
  • Nein. ​​​​​​​​​​​​​​Es muss insgesamt deutlich werden, falls fremder Code gezeigt wird.
    Wenn viel Code aus dem Originalwerk stammt, dann reicht es aus, am Anfang des Vortrags dies aufzuzeigen.
• Gilt bei allen Vorträgen Anwesenheitspflicht?
  • ​​​​​​​​​​​​​​Ja.