Verification is a domain which has for goal to expose potential design errors of programs and algorithms.Model checking is a branch of verification and is divided in three steps: modelling the system, expressing the properties the system should satisfy and effectively checking if the model satisfies the properties.For the modelling part, we will use transition system and spend some time on how to model programs. We will also see how to deal with parallel ones.Next, we will use linear temporal logic (LTL) in order to express properties of programs. We will also spend time on how to describe relevant properties in LTL. Finally for the checking if a model satisfies a property; we will study an automata based technique.
The course will be fully in English.
Die Veranstaltung wurde 1 mal im Vorlesungsverzeichnis SoSe 2025 gefunden:
