Formale Methoden können Testaufwände senken und - anders als Tests - Garantien geben, dass ein Stück Software wichtige Eigenschaften wie zum Beispiel Security und Safety erfüllt. Für formale Methoden gibt es viele Techniken und Werkzeuge - eigentlich ein Vorteil. Diese Vielfalt kann aber auch den Einstieg erschweren, weil unklar ist, welches Werkzeug das richtige für das Projekt ist.

Wir benutzen ein einen einfachen Herzschrittmacher auf Basis des Bresenham-Algorithmus, um konkret formale Methoden und ihre Werkzeuge zu demonstrieren: Model Finding, SMT-Solver, Beweisassistenten und darauf aufbauende Analysen von Quellcode. Dabei betrachten wir die präzise Formulierung der Spezifikation, die Beweisführung zur Korrektheit und den Weg zum lauffähigen Code.