Logo ČVUT
CZECH TECHNICAL UNIVERSITY IN PRAGUE
STUDY PLANS
2018/2019

Formal Methods and Specifications

Login to KOS for course enrollment Display time-table
Code Completion Credits Range Language
MIE-FME.16 Z,ZK 5 2P+1C
Lecturer:
Stefan Ratschan (guarantor)
Tutor:
Stefan Ratschan (guarantor)
Supervisor:
Department of Software Engineering
Synopsis:

After the course, students will be 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. Program specification and basics of practical logic

2. Logical theories and modeling of data structures

3. Operational program semantics

4. Bounded software model checking

5. Unbounded software model checking

6. Program termination, total program correctness

7. Symbolic program execution

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. Aaron R. Bradley and Zohar Manna: ''The Calculus of Computation'', Springer Verlag, 2007

2. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled: ''Model Checking'', MIT Press, 1999

3. Zohar Manna and Amir Pnueli: ''Temporal Verification of Reactive Systems'', Springer Verlag, 1995

4. Glynn Winskel: ''Formal Semantics of Programming Languages'', MIT Press, Cambridge, Massachusetts, 1993

Note:
Time-table for winter semester 2018/2019:
Time-table is not available yet
Time-table for summer semester 2018/2019:
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
Fri
roomT9:301
Ratschan S.
11:00–12:30
ODD WEEK

(lecture parallel1
parallel nr.101)

Dejvice
NBFIT učebna
roomTH:A-s135
Ratschan S.
12:45–14:15
(lecture parallel1)
Thákurova 7 (FSv-budova A)
As135
Thu
Fri
The course is a part of the following study plans:
Data valid to 2019-05-23
For updated information see http://bilakniha.cvut.cz/en/predmet4653106.html