Höherstufige monadenbasierte Programmierung und Verifikation

• Antragsteller: Privatdozent Dr.-Ing. Sergey Goncharov
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung seit 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 501369690

Seiteneffekte stellen für Zwecke der Programmiersprachensemantik und der Programmverfikation regelmäßig besondere Herausforderungen dar, sowohl wegen der großen Bandbreite in Betracht zu ziehender Effekte (z.B. in Gestalt von Verzweigungstypen wie Nichtdeterminismus oder Randomisierung, verschiedenen Speichermodellen wie insbesondere Heap-Speicher mit dynamischer Verlinkung, oder fortgeschrittenen Kontrollflussmechanismen) als auch wegen der mit bestimmten spezifischen Arten von Seiteneffekten verbundenen mathematischen Komplexität. Ziel von HOMBRe ist es, diesen Herausforderungen auf der richtigen Allgemeinheitsebene zu begegnen und generische semantische Konzepte, Metasprachen und Verifikationslogiken höherer Stufe für seiteneffektbehaftete Programme bereitzustellen, unter Ausnutzung zum einen des der funktional-imperativen Programmierung zugrundeliegenden Prinzips der monadenbasierten Verkapselung von Seiteneffekten und zum anderen der kategoriellen Abstraktion von Feedback-Schleifen durch sogenannte (partielle) Traces. In HOMBRe werden wir Methoden zur semantischen und logischen Analyse von Programmen höherer Ordnung mit komplexen Seiteneffekten wie insbesondere Hybridität (d.h. einer Kombination von diskretem und kontinuierlichem Verhalten, wie sie insbesondere in cyber-physikalischen Systemen anzutreffen ist) oder verschiedenen Formen dynamischer Referenzierung herausarbeiten, in Verbindung mit einer substanziellen Weiterentwicklung bestehender generischer Methoden. Als Grundlage für die Semantik von Schleifen, Fixpunkten und Rückkopplungen werden wir den von uns in eigenen Vorarbeiten eingeführten zentralen Begriff der guarded Traces verwenden, mit besonderem Augenmerk auf entsprechenden graphischen Sprachen. Ferner werden wir fortgeschrittene, insbesondere höherstufige, generische Verifikationslogiken für komplexe Berechnungsphänomene, unter anderem dynamische Referenzen und Heap-Speicher, entwerfen, die auf in unseren Vorarbeiten identifizierten semantischen Strukturen für solche Logiken sowie auf in HOMBRe neu bereitzustellenden Grundlagenresultaten aufbauen. Insbesondere werden wir Verbindungen zwischen der bestehenden Prägarbensemantik der dynamischen Referenzierung und neu zu entwickelnden Modellen auf Grundlage der nominalen Mengentheorie herstellen; nominale Mengen erlauben eine fundierte und elegante Behandlung der Allokation und Deallokation von Namen, die in diesem Zusammenhang als Speicheradressen zu verstehen sind. Wir werden die im Projekt erzielten Resultate und ihre Beweise durchgängig in Typentheorie und hierauf basierenden interaktiven Theorembeweisern formalisieren; dies verstärkt nicht nur das Vertrauen in die Korrektheit der Resultate, sondern stellt auch einen wichtigen Schritt auf dem Weg zu ihrer Verwendung in der maschinellen Verifikation dar.

• DFG-Verfahren: Sachbeihilfen