Formal Methods and Specifications

Garant předmětu:

Lecturer:

Tutor:

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. 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. Verification of unbounded program correctness

6. Termination, total program correctness

7. Formal methods for embedded systems

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

Note:

Further information:

https://moodle-vyuka.cvut.cz/course/view.php?id=2728

No time-table has been prepared for this course

The course is a part of the following study plans:

• Master branch Knowledge Engineering, in Czech, 2016-2017 (elective course)
• Master branch Computer Security, in Czech, 2016-2019 (elective course)
• Master branch Computer Systems and Networks, in Czech, 2016-2019 (elective course)
• Master branch Design and Programming of Embedded Systems, in Czech, 2016-2019 (elective course)
• Master branch Web and Software Engineering, spec. Info. Systems and Management, in Czech, 2016-2019 (elective course)
• Master branch Web and Software Engineering, spec. Software Engineering, in Czech, 2016-2019 (compulsory course of the branch)
• Master branch Web and Software Engineering, spec. Web Engineering, in Czech, 2016-2019 (elective course)
• Master program Informatics, unspecified branch, in Czech, version 2016-2019 (VO)
• Master branch System Programming, spec. System Programming, in Czech, 2016-2019 (elective course)
• Master branch System Programming, spec. Computer Science, in Czech, 2016-2017 (elective course)
• Master specialization Computer Science, in Czech, 2018-2019 (elective course)
• Master branch Knowledge Engineering, in Czech, 2018-2019 (elective course)