Bachelorseminar Programsynthese

Beschreibung

Inhalte

Programme ohne Programmierung - eine Vorstellung,
die bereits in den Anfangstagen der Informatik diskutiert wurde:
Statt eines Algorithmus, der angibt “wie” ein Problem gelöst wird,
beschreibt man nur “was” die gültigen Lösungen sind,
z.B. als eine Spezifikation in Logik, oder als eine Menge von konkreten
Beispielen.

Es gibt viele Ansätze und Techniken, die diesen Traum für bestimmte
Anwendungsfälle wahr werden lassen. Ein klassisches Beispiel für solch
“deklarative” ist Prolog, moderne Ansätze können aber viel mehr.

In diesem Seminar stellen die SeminarteilnehmerInnen jeweils einen Ansatz
oder ein wissenschaftliches Papier vor und experimentieren mit den
jeweiligen dazugehörigen Tools und Programmiersprachen.

Empfohlene Vorkenntnisse:
- Formale Spezifikation und Verifikation
- Logik und Diskrete Strukturen

Anforderungen

  • selbstständige Literaturrecherche
  • eigensständige praktische Experimente mit den Tools
  • mündliche Präsentation (ca 20 min)
  • schriftliche Ausarbeitung (ca 8-10 Seiten im LNCS
    Format    )

Hinweis: Sie sind selbst verantwortlich für das Einhalten guter
wissenschaftlicher Praxis, dazu gehört korrektes Zitieren in allen Dokumenten
(Präsentation, Text, auch im Entwurf!), Verstöße führen direkt zum
nicht-Bestehen des Seminars. Wir besprechen die Regeln eingangs ganz konkret.
Mit eigenen Worten und einer eigenen Struktur werden Sie diese Regeln leicht
einhalten können.

Themenliste (vorläufig)

  • Logikprogrammierung mit Prolog (PROLOG programming in depth, Kapitel 1 + 3, sowie eine Anwendung, 1995)
  • Two-stage technique for LTLf synthesis under LTL assumptions (KR 2020)
  • Synthesis of LTL formulas from natural language texts: State of the art and research directions (TIME 2019)
  • GitHub Copilot (Evaluating Large Language Models Trained on Code, arXiv, 2021)
  • Synchronous programming of reactive systems: an introduction to ESTEREL (INRIA, 1987, Tool: Ceu)
  • Relational E-Matching (POPL 2022)
  • Supercompilation (Stochastic superoptimization, ASPLOS 2013)
  • Cyclic Program Synthesis (PLDI 2021)
  • An overview of the Leon verification system (Scala 2013)
  • Syntaxgetriebene Synthese z.B. mit CVC5 (Syntax-guided Synthesis, FMCAD 2013)
  • The sketching approach to program synthesis (ASPLOS 2009)
  • Data Migration using Datalog Program Synthesis (VLDB 2020)
  • Learning Compositional Rules via Neural Program Synthesis (NeurIPS 2020)
  • Program synthesis from polymorphic refinement types (PLDI 2016)
  • Higher order unification 30 years later (TPHOLS abstract 2002)
  • Learning to prove theorems via interacting with proof assistants (PMLR 2019)
  • Synthesizing Analytical SQL Queries from Computation Demonstration (arXiv 2022)

Semesterplan (vorläufig)

    1. April: Vorbesprechung
    1. Mai: Themenvergabe + Tips zur Literaturrecherche
    1. Mai: Aspekte guter Präsentation
    1. Mai: Lightning Talks
    1. Mai: Hinweise zur Ausarbeitung
    1. Mai: fällt aus

Präsentationen (je 2 pro Termin)

    1. Juni - 5. Juli
    1. Juli: fällt aus
    1. Juli: ?
    1. Juli: ?
Institut
Institut für Informatik
Dozent:in
Assistent:in
Kursteilnehmer:innen
10 von 10
Zentralanmeldung
Bachelorseminare
Anweisungen zur Anmeldung

Bitte keine zusätzlichen Bewerbungen einreichen, wir nehmen keinen Einfluss auf die Verteilung der Seminarplätze.

Material

Das Kursmaterial ist nur für Mitglieder des Kurses einsehbar, also z.B. für Teilnehmer:innen, Tutor:innen, Korrektor:innen und Verwalter:innen.

Prüfungen
NameAnmeldung abAnmeldung bisTerminPrüfungsanmeldung
Seminarnote
Nicht zur Prüfung angemeldet
Termine
ArtZeitRegulärer RaumNotiz
Seminar
  • Di 12:15–14:00
Oettingenstr C 003