05.07.2025 –, V1 (F119)
Manche Software hat besondere Anforderungen - nicht nur an das Design sondern auch die Korrektheit der Realisierung. Leider sind Entwicklungsprozesse oft fehleranfällig, und bekanntermaßen können alle Tests der Welt nur die Anwesenheit von Fehlern zeigen, nicht aber deren Abwesenheit.
Glücklicherweise sind in den letzten Jahren die sogenannten formalen Methoden und ihre Werkzeuge immer zugänglicher geworden. Diese Methoden werden inzwischen auch in größeren Projekten angewandt und liefern mathematische Beweise, dass die Software kritische, explizit formulierte Anforderungen auch garantiert erfüllt. Dafür werden die kritischen Eigenschaften in den Code aufgenommen und verifiziert.
Im Vortrag geht es speziell darum, Code mit Hilfe mathematisch korrekt zu beweisen. Im Studium macht man das gelegentlich an Spielzeugbeispielen und lernt es dort als mühsame Plackerei kennen: Mit Hilfe moderner Open-Source-Werkzeuge - sogenannter Beweisassistenten - geht es nicht nur leichter von der Hand, sondern macht auch richtig Laune.
Der Vortrag zeigt, wo der Einsatz solcher Werkzeuge sinnvoll ist und wie ihr Einsatz in der Praxis abläuft.
grundlegende Programmierkenntnisse
Dr. Michael Sperber ist Geschäftsführer der Active Group GmbH, die Individualsoftware mit funktionaler Programmierung entwickelt. Er ist international anerkannter Experte für funktionale Programmierung und wendet sie seit über 20 Jahren in Forschung, Lehre und industrieller Entwicklung an. Außerdem hat er zahlreiche Fachartikel und Bücher zum Thema verfasst, sowie das Curriculum für das iSAQB-Advanced-Modul "Formale Methoden" (zusammen mit Lars Hupel). Michael Sperber ist Mitbegründer des Blogs funktionale-programmierung.de und Mitorganisator der Entwicklerkonferenz BOB.