Logo ČVUT
CZECH TECHNICAL UNIVERSITY IN PRAGUE
STUDY PLANS
2023/2024
UPOZORNĚNÍ: Jsou dostupné studijní plány pro následující akademický rok.

Formal Methods and Specifications

Login to KOS for course enrollment Display time-table
Code Completion Credits Range Language
NI-FME Z,ZK 5 2P+1C Czech
Garant předmětu:
Stefan Ratschan
Lecturer:
Stefan Ratschan
Tutor:
Stefan Ratschan
Supervisor:
Department of Software Engineering
Synopsis:

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.

Requirements:

Knowledge of basic notions of mathematical logic and set theory and ability to use them.

Syllabus of lectures:

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

Syllabus of tutorials:

Practical training of the lecture material.

Study Objective:

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.

Study materials:

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.

Note:
Further information:
https://moodle.fit.cvut.cz/courses/MI-FME.16/
Time-table for winter semester 2023/2024:
Time-table is not available yet
Time-table for summer semester 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
Mon
Tue
Wed
roomTH:A-s134
Ratschan S.
09:15–10:45
(lecture parallel1)
Thákurova 7 (budova FSv)
As134
roomT9:302
Ratschan S.
12:45–14:15
EVEN WEEK

(lecture parallel1
parallel nr.101)

Dejvice
NBFIT učebna
roomT9:302
Ratschan S.
14:30–16:00
EVEN WEEK

(lecture parallel1
parallel nr.102)

Dejvice
NBFIT učebna
Thu
Fri
The course is a part of the following study plans:
Data valid to 2024-03-27
Aktualizace výše uvedených informací naleznete na adrese https://bilakniha.cvut.cz/en/predmet6114806.html