HOME | ENGLISH | IMPRESSUM | KIT

Bachelorarbeit (abgeschlossen): Formal verifiziertes Einfügen von Referenzzählungsinstruktionen

Bei der Implementierung funktionaler Sprachen ist heutzutage eine automatische Speicherverwaltung in Form eines Tracing Garbage Collectors Standard und hat frühere Implementierungen mittels Referenzzählung weitestgehend abgelöst. Im Spezialfall von pur funktionalen Sprachen kann optimierte Referenzzählung aber auch heute noch kompetitive Laufzeiten ergeben, wie unserem Paper gezeigt. Ein Bestandteil davon ist eine Intermediate Representation, die explizite Instruktionen zur Referenzzählung enthält, sowie ein Compiler in diese. Die Arbeitsweise des Compilers wurde in einem vorläufigen Appendix relativ zu einem Typsystem als korrekt bewiesen; jedoch ist dabei eine technische Komplexität erreicht, bei der Papierbeweise nicht mehr unbedingt vertrauenswürdig sind. In dieser Arbeit sollen daher der Beweis und dafür benötigte Konstruktionen wie das Typsystem im Theorembeweiser Lean formalisiert werden, um eine vertrauenswürdigere Korrektheitsaussage zu erhalten.

Aufgabe:

Formalisierung des Compilerbeweises und benötigter Abhängigkeiten aus obigem Appendix in Lean

Voraussetzungen

  • Grundkenntnisse in formalen Systemen

Schlüsselworte

Lean, Programmverifikation, Compiler 

Veröffentlichungen

Veröffentlichung
Formally Verified Insertion of Reference Counting Instructions

Betreuer

Wissenschaftliche Mitarbeiter
Sebastian Ullrich

Studenten

Ehemalige Tutoren
Marc Huisinga