IA169 System Verification and Assurance

Faculty of Informatics
Autumn 2021
Extent and Intensity
2/0/2. 4 credit(s) (plus extra credits for completion). Type of Completion: zk (examination).
Teacher(s)
prof. RNDr. Jiří Barnat, Ph.D. (lecturer)
RNDr. Marek Chalupa, Ph.D. (seminar tutor)
doc. RNDr. Vojtěch Řehák, Ph.D. (seminar tutor)
prof. RNDr. Václav Matyáš, M.Sc., Ph.D. (assistant)
Guaranteed by
prof. RNDr. Jiří Barnat, Ph.D.
Department of Computer Science – Faculty of Informatics
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Wed 15. 9. to Wed 8. 12. Wed 16:00–17:50 D1
  • Timetable of Seminar Groups:
IA169/Konzultace_k_DU: Mon 13. 9. to Mon 6. 12. Mon 16:00–17:50 A219, J. Barnat, V. Řehák
Prerequisites
(! IV113 Validation and Verification ) && (!NOW( IV113 Validation and Verification ))
User-level familiarity with Unix/Linux operating system. Basic programming skills (Python). Some degree of abstract 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 130 student(s).
Current registration and enrolment status: enrolled: 2/130, only registered: 0/130, only registered with preference (fields directly associated with the programme): 0/130
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. 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.
Learning outcomes
Students will:
be aware of fundaments of black-box testing;
understand priciples of deductive verification;
understand the theory and application of model checking;
have hand-on experince with a couple of verification tools.
Syllabus
  • This course will provide the necessary theoretic background as well as hands-on experience with relevant tools for bug finding and formal verification techniques. The core topics of this course will include testing, symbolic execution, abstract interpretation, static analysis, theorem proving, automated formal verification as well as an introduction to model-based verification. 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. An introductory insight into security standards like Common Criteria for Information Technology Security Evaluation and FIPS 140 shall be provided as well.
Literature
  • GRUMBERG, Orna, Doron A. PELED and E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
Teaching methods
lectures, homework assignments, readings
Assessment methods
Final (written) exam: 50%. Assignments: 50%.
Marking scheme: A for 85% or higher, then B for 80% or higher, then C for 75% or higher, then D for 70% or higher, then E for 65% or higher, then F(ail) for less than 65%.
Colloquy or credit – at least 65%.
Language of instruction
English
Follow-Up Courses
Further Comments
Study Materials
The course is taught annually.
The course is also listed under the following terms Spring 2016, Spring 2017, Spring 2018, Spring 2019, Autumn 2019, Autumn 2020, Autumn 2022, Spring 2024.
  • Enrolment Statistics (Autumn 2021, recent)
  • Permalink: https://is.muni.cz/course/fi/autumn2021/IA169