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. Mgr. Jan Obdržálek, PhD. (lecturer)
- Guaranteed by
- prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science - Faculty of Informatics
Contact Person: doc. Mgr. Jan Obdržálek, PhD.
Supplier department: Department of Computer Science - Faculty of Informatics
- Mon 12:00–13:50 G123
- 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 of basic formal verification methods, namely model checking methods, reachability analysis, symbolic execution, abstract interpretations, and theorem proving;
make reasoned decisions about suitability of various methods for verification of specific systems;
- Overview of formal verification methods.
- Software testing.
- Deductive verification methods (theorem proving).
- LTL model checking of finite and infinite-state systems.
- State explosion problem, partial order reduction, abstraction.
- Counter-example guided abstraction refinement.
- 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.