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

Formální metody a specifikace

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

Studenti dokážou formálně popisovat sémantiku programů a používat logické uvažování pro konstrukci správně fungujícího programu. Naučí se principy softwarových nástrojů, které slouží k dokazování základních vlastností algoritmů.

Požadavky:

Znalost základních pojmů matematické logiky a teorie množin, schopnost je používat.

Osnova přednášek:

1. Úvod do formální specifikace programů.

2. Dokazovací metody.

3. Logické teorie a modelování datových struktur.

4. Operační sémantika programů.

5. Ověření omezené správnosti programů.

6. Ověření neomezené správnosti programů.

7. Funkce, procedury.

8. Důkazy terminace.

9. Symbolické provádění.

10. Rozhodovací procedury.

11. Objektově orientované programování.

12. Syntéza programů.

Osnova cvičení:

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

Cíle studia:

Cílem předmětu je poskytnout studentům schopnost používat formální způsoby uvažování při vývoji software. To na jednu stranu zahrnuje schopnost založit své vlastní vývojářské činnosti na logickém úsudku, a to i v prostředí, ve kterém se nepoužívají formální metody. Na druhou stranu to zahrnuje schopnost používání automatizovaných formálních metod a přístrojů, které podporují proces vývoje softwaru.

Studijní materiály:

1. Clarke, E.M. - Henzinger, Th.A. - Veith, H. - Bloem, R. (Eds.) : Handbook of Model Checking. Springer, 2018. ISBN 978-3-319-10574-1.

2. Kroening, D. - Strichman, O. : Decision Procedures - An Algorithmic Point of View, 2nd edition. Springer, 2016. ISBN 978-3-662-50496-3.

3. Bradley, A. R. - Manna, Z. : The Calculus of Computation. Springer, 2007. ISBN 978-3-540-74113-8.

Poznámka:

Informace o předmětu a výukové materiály naleznete na https://moodle.fit.cvut.cz/courses/MI-FME.16/

Další informace:
https://moodle.fit.cvut.cz/courses/MI-FME.16/
Rozvrh na zimní semestr 2022/2023:
Rozvrh není připraven
Rozvrh na letní semestr 2022/2023:
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 TH:A-s134
Ratschan S.
09:15–10:45
(přednášková par. 1)
Thákurova 7 (FSv-budova A)
As134
místnost T9:346
Ratschan S.
12:45–14:15
LICHÝ TÝDEN

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

Dejvice
NBFIT učebna
místnost T9:347
Ratschan S.
14:30–16:00
LICHÝ TÝDEN

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

Dejvice
NBFIT učebna
Čt

Předmět je součástí následujících studijních plánů:
Platnost dat k 29. 1. 2023
Aktualizace výše uvedených informací naleznete na adrese https://bilakniha.cvut.cz/cs/predmet6114806.html