Formale Methoden der Softwareentwicklung 2016/2017 /KursID:739
- Letzter Beitrag vom 2017-02-09

Lehrende(r)

Dr. Tadeusz Litak

Einrichtung

Lehrstuhl für Informatik 8 (Theoretische Informatik)

Aufzeichnungsart

Vorlesungsreihe

Zugang

Frei

Sprache

In the first part of the course, we will engage in the formal verification of reactive systems. Students learn the syntax and semantics of the temporal logics LTL, CTL, and CTL* and their application in the specification of e.g. safety and liveness properties of systems. Simple models of systems are designed and verified using model checkers and dedicated frameworks for asynchronous and synchronous reactive systems, and the algorithms working in the background are explained.

The second part of the course focuses on functional correctness of programs; more precisely, we discuss the theory of pre- and postconditions, Hoare triples, loop invariants, and weakest (liberal) preconditions, in order to introduce automatised correctness proofs using the Hoare calculus.

 

Students are going to acquire the following competences:

Wissen
  • Reproduce the definition of syntax and semantics of temporal logics LTL, CTL, and CTL*.
  • Reproduce the definition of semantics of a simple programming languages like IMP, with special focus on axiomatic semantics (Hoare rules).

  • Explain how CTL can be characterised in terms of fixpoints.

Verstehen
The students understand the workings of state of the art automatic frameworks, clarifying the role of model checking algorithms, semantics and Hoare calculi in formal verification.
Anwenden
In a series of exercises, the students use state of the art tools for
  • model checking

  • specification and verification of reactive systems,

  • verification of functional correctness or memory safety of simple programs.

Analysieren
  • Choose the optimal tool for a given verification or specification problem.
  • Differentiate between safety and liveness properties.

Zugehörige Einzelbeiträge

Folge
Titel
Lehrende(r)
Aktualisiert
Zugang
Dauer
Medien
1
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2016-10-19
Frei
01:21:23
2
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2016-10-26
Frei
01:21:21
3
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2016-10-28
Frei
01:37:07
4
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2016-11-02
Frei
01:26:45
5
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2016-11-04
Frei
01:16:47
6
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2016-11-09
Frei
01:24:20
7
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2016-11-16
Frei
01:21:42
8
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2016-11-23
Frei
01:28:23
9
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2016-11-25
Frei
00:55:00
10
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2016-11-30
Frei
01:27:19
11
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2016-12-02
Frei
00:53:43
12
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2016-12-07
Frei
01:29:07
13
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2016-12-16
Frei
01:23:57
14
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2016-12-16
Frei
01:23:57
15
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2017-01-11
Frei
01:24:29
16
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2017-01-20
Frei
01:29:26
17
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2017-01-25
Frei
01:25:17
18
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2017-02-01
Frei
01:24:24
19
Formale Methoden der Softwareentwicklung
Dr. Tadeusz Litak
2017-02-09
Frei
01:24:44

Mehr Kurse von Dr. Tadeusz Litak

Schloss1
Dr. Tadeusz Litak
Vorlesung
2019-11-18
Passwort
Schloss1
Dr. Tadeusz Litak
Vorlesung
2020-07-22
Passwort
Milius, Stefan
Dr. Tadeusz Litak
Vorlesung
2019-07-24
IdM-Anmeldung
Schloss1
Dr. Tadeusz Litak
Vorlesung
2019-07-25
Passwort

Mehr Kurse aus der Kategorie "Technische Fakultät"

Schloss1
Prof. Dr. Emanuël Habets
Vorlesung
2024-02-02
IdM-Anmeldung
Schloss1
Dr. Volkmar Sieh
Übung
2021-04-12
IdM-Anmeldung
Schloss1
Prof. Dr. Walter Kellermann
Vorlesung
2020-06-28
Studon
Wierschem, Andreas
Prof. Dr. Andreas Wierschem
Vorlesung
2020-06-29
Studon
Willner, Kai
Prof. Dr. Kai Willner
Vorlesung
2017-01-19
Frei