Logo ČVUT
ČESKÉ VYSOKÉ UČENÍ TECHNICKÉ V PRAZE
STUDIJNÍ PLÁNY
2023/2024
UPOZORNĚNÍ: Jsou dostupné studijní plány pro následující akademický rok.

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
Garant předmětu:
Stefan Ratschan
Přednášející:
Stefan Ratschan
Cvičící:
Stefan Ratschan
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 2023/2024:
Rozvrh není připraven
Rozvrh na letní semestr 2023/2024:
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 (budova FSv)
As134
místnost T9:302
Ratschan S.
12:45–14:15
SUDÝ TÝDEN

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

Dejvice
NBFIT učebna
místnost T9:302
Ratschan S.
14:30–16:00
SUDÝ 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 22. 4. 2024
Aktualizace výše uvedených informací naleznete na adrese https://bilakniha.cvut.cz/cs/predmet6114806.html