Formale Methoden in der Praxis: SMT Solver und Model Checker

Formale Analyse und Verifikation von Modellen und Programmen werden von vielen Praktikern als „zu kompliziert" oder „praxisuntauglich" verschmäht. Für manche Ansätze mag das stimmen, für andere definitiv nicht. Dieser Vortrag gibt einen Überblick über zwei Verifikationsansätze, die wir in der Praxis verwenden: SMT Solver und Model Checker. Wir illustrieren, wo und wie man sie auf Modellen und Code einsetzen kann, und dass sie eine für Praktiker sinnvolle Ergänzung zum Testen sein können.

Zielpublikum: Entwickler
Voraussetzungen: Solide Programmierkenntnisse
Schwierigkeitsgrad: Anfänger