Separation logic ist eine Logik zum einfacheren Verifizieren imperativer Programme. Das
Iris-Projekt bietet eine benutzerfreundliche Schnittstelle an, um mit Beweisen in solch einer Logik im Theorembeweiser Coq zu interagieren. Ziel dieser Arbeit ist es, eine ähnliche Schnittstelle im Theorembeweiser Lean, der an unserem Lehrstuhl mitentwickelt wird, zu implementieren und dabei insbesondere relevante Unterschiede zwischen Lean und Coq zu erforschen und ggf. entsprechende Verbesserungen an der Schnittstelle anzubringen.
Schlüsselworte
Lean, separation logic, Iris
Veröffentlichungen
Betreuer
Studenten
