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

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
NIE-FME Z,ZK 5 2P+1C anglicky
Přednášející:
Stefan Ratschan (gar.)
Cvičící:
Stefan Ratschan (gar.)
Předmět zajišťuje:
katedra softwarového inženýrství
Anotace:

Students are 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. Introduction to formal program specification

2. Proof methods

3. Logical theories and modeling of data structures

4. Operational program semantics

5. Unbounded software model checking

6. (2) Unbounded software model checking

7. Functions, procedures

8. Termination proofs

9. Symbolic execution

10. Decision procedures

11. Object oriented programming

12. Program synthesis

Osnova cvičení:

Practical training of the lecture material.

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. 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:

Information about the subject and teaching materials can be found at https://courses.fit.cvut.cz/NI-FME/

Další informace:
https://courses.fit.cvut.cz/NI-FME/
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
SUDÝ TÝDEN

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

Dejvice
NBFIT učebna
Čt

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