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

Formální metody a specifikace

Předmět není vypsán Nerozvrhuje se
Kód Zakončení Kredity Rozsah Jazyk výuky
NI-FME Z,ZK 5 2P+1C česky
Přednášející:
Cvičící:
Předmět zajišťuje:
katedra softwarového inženýrství
Anotace:

Studenti dokážou formálně popisovat sémantiku software a používat logické uvažování pro konstrukci správně fungujícího software. Naučí se použít některé programové nástroje, které slouží pro dokazování vlastností softwaru.

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. (2) 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/
Pro tento předmět se rozvrh nepřipravuje
Předmět je součástí následujících studijních plánů:
Platnost dat k 10. 7. 2020
Aktualizace výše uvedených informací naleznete na adrese http://bilakniha.cvut.cz/cs/predmet6114806.html