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

• 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 hinzuzufügen, ohne den Datentyp ändern zu müssen. Wenn man einem 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 Votragszeit + 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!