Michael Sperber und Lars Hupel erörtern, warum formale Methoden für die Gewähr­leistung der Korrektheit von Software unerlässlich sind, insbe­sondere bei sicher­heits­kri­ti­schen Systemen. Das Modul vermittelt, wie diese mathe­ma­ti­schen Techniken in den Entwick­lungs­prozess integriert werden können, um die Zuver­läs­sigkeit zu gewährleisten.