FI:IA159 Formal Verification Methods - Course Information
IA159 Formal Verification MethodsFaculty of Informatics
- Extent and Intensity
- 2/0. 2 credit(s) (plus extra credits for completion). Type of Completion: zk (examination).
- doc. RNDr. Jan Strejček, Ph.D. (lecturer)
- Guaranteed by
- prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science - Faculty of Informatics
Supplier department: Department of Computer Science - Faculty of Informatics
- Thu 12:00–13:50 B410
- IA006 Automata theory
It is recommended to attend courses IA040 Modal and Temporal Logics for Processes and IV113 Introduction to Validation and Verification before registering this course.
- Course Enrolment Limitations
- The course is also offered to the students of the fields other than those the course is directly associated with.
- fields of study / plans the course is directly associated with
- there are 18 fields of study the course is directly associated with, display
- Course objectives
- At the end of this course, students should be able to: understand and explain principles, advantages, and disadvantages of basic formal verification methods, namely model checking methods, symbolic execution, abstract interpretation, and theorem proving;
make reasoned decisions about suitability of various methods for verification of specific systems;
- Overview of formal verification methods.
- Deductive verification methods (theorem proving).
- LTL model checking of finite and infinite-state systems.
- Counter-example guided abstraction refinement.
- Bounded model checking.
- Symbolic execution.
- Static analysis, abstract interpretation.
- Verification tools.
- Teaching methods
- Assessment methods
- oral exam
- Language of instruction
- Further Comments
- Study Materials
The course is taught annually.