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
- Wed 12:00–13:50 A318
- Prerequisites (in Czech)
- IV113 Validation and Verification || IA169 System Verif. and Assurance
- 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 19 fields of study the course is directly associated with, display
- Course objectives
- At the end of this course, students should understand and be able to explain principles, advantages, and disadvantages of selected from the area of formal verification, namely model checking methods, abstraction, static analysis via abstract interpretation, and shape analysis;
make reasoned decisions about suitability of various methods for verification of specific systems;
- Overview of formal verification methods.
- LTL model checking of finite and infinite-state systems including translation of LTL to Büchi automata and partial order reduction.
- Counter-example guided abstraction refinement.
- Static analysis, abstract interpretation.
- Shape analysis.
- Software verification via automata, symbolic execution, and interpolation.
- Teaching methods
- Assessment methods
- oral exam
- Language of instruction
- Further Comments
- Study Materials
The course is taught annually.