Proseminar: Formale Methoden

Der Begriff formale Methoden steht für Sprachen und Methoden die es erlauben, Systeme auf bestimmten Abstraktionsebenen mit mathematischen Mitteln präzise zu modellieren, Anforderungen an sie zu formulieren und die Erfüllung dieser Eigenschaften zuverlässig zu analysieren.

In diesem Proseminar behandeln wir einige grundlegende Themen aus dem Bereich der formalen Methoden, wie zum Beispiel Modellierungssprachen für Systeme (unterschiedliche Klassen von Automaten für diskrete, hybride und probabilistische Systeme), Spezifikationssprachen für Eigenschaften (temporäre Logiken wie z.B. CTL*, CTL, LTL, MTL, Hyperproperties), Verifikationstechniken (Deduktion, Model Checking, Bounded Model Checking), aber auch Techniken die in Verifikationsprozessen Verwendung finden (Satisfiability Checking).