FI:IA169 System Verif. and Assurance - Course Information
IA169 System Verification and AssuranceFaculty of Informatics
- Extent and Intensity
- 2/2/2. 6 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium), z (credit).
- prof. RNDr. Jiří Barnat, Ph.D. (lecturer)
doc. RNDr. Vojtěch Řehák, Ph.D. (lecturer)
prof. RNDr. Václav Matyáš, M.Sc., Ph.D. (lecturer)
Mgr. Marek Chalupa (seminar tutor)
- Guaranteed by
- prof. RNDr. Václav Matyáš, M.Sc., Ph.D.
Department of Computer Science - Faculty of Informatics
Supplier department: Department of Computer Science - Faculty of Informatics
- Tue 19. 2. to Tue 14. 5. Tue 12:00–13:50 A319
- Timetable of Seminar Groups:
IA169/02: Mon 10:00–11:50 A219, M. Chalupa, V. Řehák
- (! IV113 Validation and Verification ) && (! NOW ( IV113 Validation and Verification ))
User-level familiarity with Unix/Linux operating system. Basics of C programming. Basic astract math reasoning.
- Course Enrolment Limitations
- The course is also offered to the students of the fields other than those the course is directly associated with.
The capacity limit for the course is 32 student(s).
Current registration and enrolment status: enrolled: 14/32, only registered: 0/32, only registered with preference (fields directly associated with the programme): 0/32
- fields of study / plans the course is directly associated with
- Course objectives
- The student will understand the necessary theoretic background as well as acquire hands-on experience with relevant tools for bug finding and formal verification techniques. With the help of a tutor students will get acquainted with a number of concrete software verification tools for analysis of concurrent systems, real-time systems, hybrid systems, cryptographic systems and systems with probabilities.
- This course will provide the necessary theoretic background as well as hands-on experience with relevant tools for bug finding and formal verification techniques. An introductory insight into security standards like Common Criteria for Information Technology Security Evaluation and FIPS 140 shall be provided first, together with a discussion of security threat models. Following this, the core topics of this course will include testing, simulations, advance testing and symbolic execution, abstract interpretation, static analysis, theorem proving, automated formal verification as well as an introduction to model-based verification. With the help of a tutor students will get acquainted with a number of concrete software verification tools for analysis of concurrent systems, real-time systems, hybrid systems, cryptographic systems and systems with probabilities.
- Teaching methods
- lectures, seminars/labs, homework assignments, readings
- Assessment methods
- Final (written) exam: 70%. Assignments: 30%.
Marking scheme: A for 90% or higher, then B for 80% or higher, then C for 70% or higher, then D for 60% or higher, then E for 50% or higher, then F(ail) for less than 50%.
Colloquy or credit – at least 44%.
- Language of instruction
- Follow-Up Courses
- Further Comments
- Study Materials
The course is taught annually.
- Listed among pre-requisites of other courses