Logo ČVUT
ČESKÉ VYSOKÉ UČENÍ TECHNICKÉ V PRAZE
STUDIJNÍ PLÁNY
2018/2019

Formal Methods and Specifications

Přihlášení do KOSu pro zápis předmětu Zobrazit rozvrh
Kód Zakončení Kredity Rozsah Jazyk výuky
MIE-FME.16 Z,ZK 5 2P+1C
Přednášející:
Stefan Ratschan (gar.)
Cvičící:
Stefan Ratschan (gar.)
Předmět zajišťuje:
katedra softwarového inženýrství
Anotace:

After the course, students will able to describe semantics of software formally and to use sound reasoning for construction of correct software. They learn to use some software tools that allow to prove basic properties of software.

Požadavky:

Knowledge of basic notions of mathematical logic and set theory and ability to use them.

Osnova přednášek:

1. Program specification and basics of practical logic

2. Logical theories and modeling of data structures

3. Operational program semantics

4. Bounded software model checking

5. Unbounded software model checking

6. Program termination, total program correctness

7. Symbolic program execution

Osnova cvičení:

Cvičení materiálu z přednášky.

Cíle studia:

The goal of the module is to provide students with the ability to apply formal reasoning in software development. On one hand, this includes the ability to base their own software development activities on sound reasoning, even within an environment that does not systematically employ formal methods. On the other hand, this includes the ability to understand and use automated techniques and tools for supporting formal methods within the software development process.

Studijní materiály:

1. Aaron R. Bradley and Zohar Manna: ''The Calculus of Computation'', Springer Verlag, 2007

2. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled: ''Model Checking'', MIT Press, 1999

3. Zohar Manna and Amir Pnueli: ''Temporal Verification of Reactive Systems'', Springer Verlag, 1995

4. Glynn Winskel: ''Formal Semantics of Programming Languages'', MIT Press, Cambridge, Massachusetts, 1993

Poznámka:

Rozsah: 2p+1c

Rozvrh na zimní semestr 2018/2019:
Rozvrh není připraven
Rozvrh na letní semestr 2018/2019:
06:00–08:0008:00–10:0010:00–12:0012:00–14:0014:00–16:0016:00–18:0018:00–20:0020:00–22:0022:00–24:00
Po
Út
St
místnost T9:301
Ratschan S.
11:00–12:30
LICHÝ TÝDEN

(přednášková par. 1
paralelka 101)

Dejvice
NBFIT učebna
místnost TH:A-s135
Ratschan S.
12:45–14:15
(přednášková par. 1)
Thákurova 7 (FSv-budova A)
As135
Čt

Předmět je součástí následujících studijních plánů:
Platnost dat k 23. 5. 2019
Aktualizace výše uvedených informací naleznete na adrese http://bilakniha.cvut.cz/cs/predmet4653106.html