Formální metody a specifikace

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) As134místnost T9:302 Ratschan S. 12:45–14:15 SUDÝ TÝDEN (přednášková par. 1 paralelka 101) Dejvice NBFIT učebnamí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á

Předmět je součástí následujících studijních plánů:

• Mgr. specializace Počítačová bezpečnost, 2020 (volitelný předmět)
• Mgr. specializace Návrh a programování vestavných systémů, 2020 (volitelný předmět)
• Mgr. specializace Počítačové systémy a sítě, 2020 (volitelný předmět)
• Mgr. specializace Manažerská informatika, 2020 (volitelný předmět)
• Mgr. specializace Softwarové inženýrství, 2020 (PS)
• Mgr. specializace Systémové programování, verze od 2020 (volitelný předmět)
• Mgr. specializace Webové inženýrství, 2020 (volitelný předmět)
• Mgr. specializace Znalostní inženýrství, 2020 (volitelný předmět)
• Mgr. specializace Teoretická informatika, 2020 (volitelný předmět)
• Mgr. program, pro fázi studia bez specializace, ver. pro roky 2020 a vyšší (VO)
• Master Specialization Digital Business Engineering, 2023 (VO)
• Mgr. specializace Systémové programování, verze od 2023 (volitelný předmět)
• Mgr. specializace Teoretická informatika, 2023 (volitelný předmět)