|
Lecturer(s)
|
-
Jančar Petr, prof. RNDr. CSc.
|
|
Course content
|
The course aims at a deep understanding of formal methods in particular in the area of automated verification of systems. It comprises, e.g., the following parts: Logic and partially automated theorem proving. Modelling software and hardware systems. Formal specification, temporal logic and automata. Automated verification, model checking. Process algebras and equivalences. Software verification tools.
|
|
Learning activities and teaching methods
|
|
Dialogic Lecture (Discussion, Dialog, Brainstorming), Work with Text (with Book, Textbook)
|
|
Learning outcomes
|
Students get familiar with basic methods of verification of software and hardware systems.
1. Knowledge Understanding principles of formal verification and its practical application.
|
|
Prerequisites
|
unspecified
|
|
Assessment methods and criteria
|
Oral exam
Completing the assignments. Passing the exam.
|
|
Recommended literature
|
-
Clarke E.M., Grumberg O., Peled D. (1999). Model Checking. MIT Press.
-
Clarke, E.M., Henzinger, Th.A., Veith, H., Bloem, R. (Eds). (2018). Handbook of Model Checking. Springer.
-
Manna Z. (1981). Matematická teorie programů. SNTL Praha.
-
Schneider K. (2004). Verification of Reactive Systems (Formal Methods and Algorithms). Springer.
|