Ferienakademie 2024
OshrEQ: Crafting your Homework Proof Mate
Hast du schon einmal darüber nachgedacht, wie man die Korrektheit von Programmtransformationen rigoros nachweisen kann?
Hast du dich gefragt, wie leistungsstarke Beweisassistenten wie Isabelle oder Coq funktionieren, deren Einsatzgebiete von der Verifikation des Betriebssystemkerns bis zur zertifizierten Kompilierung reichen?
Nichts ist so wertvoll wie das, was mit eigenen Händen gemacht wird! In diesem Kurs tauchen wir ein in die spannende Welt des Programmierens von zertifizierten Beweisen über Programme. Technischer Hintergrund für diesen Kurs ist, dass in der Vorlesung “Functional Programming and Verification” an der TUM ein kleines Regelsystem vorgestellt wird, mit dessen Hilfe die Äquivalenz von OCaml-Ausdrücken bewiesen werden kann. Solche Beweise sind sehr schematisch. Weil man auf dem Papier aber ständig Fehler macht, soll ein kleines System implementiert werden, das bei der Erstellung von Beweisen hilft, z.B. indem es prüft, ob man die Regeln richtig angewendet hat. Man kann sich natürlich auch noch mehr Automatisierung vorstellen, z.B., dass OshrEQ die Regeln selbst anwendet … hier sind der Fantasie keine Grenzen gesetzt.
Komm zu unseren Kurs bei der Ferienakademie 2024 (22. September 2024 – 4. Oktober 2024) in den wunderschönen Sarntaler Alpen in Südtirol. Der Kurs richtet sich an fortgeschrittene Bachelor- und Masterstudierende mit Programmierkenntnissen, insbesondere in OCaml.
Bewirb dich bis zum 1. Mai 2024 über die Website der Ferienakademie. Wir freuen uns auf deine Teilnahme an diesem außergewöhnlichen Ereignis!