IA169 Model Checking
Faculty of InformaticsSpring 2025
- Extent and Intensity
- 2/1/0. 3 credit(s) (plus extra credits for completion). Type of Completion: zk (examination).
In-person direct teaching - Teacher(s)
- prof. RNDr. Jan Strejček, Ph.D. (lecturer)
RNDr. Martin Jonáš, Ph.D. (seminar tutor) - Guaranteed by
- prof. RNDr. Jan Strejček, Ph.D.
Department of Computer Science – Faculty of Informatics
Supplier department: Department of Computer Science – Faculty of Informatics - Prerequisites
- 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: 0/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
- there are 30 fields of study the course is directly associated with, display
- Course objectives
- The student will understand the fundamental and currently used model checking algorithms and techniques (except those primarily designed for software). Further, the student will be able to read and write specifications in LTL and CTL, and use relevant formalisms like Büchi automata and binary decision diagrams.
- Learning outcomes
- Students will:
understand traditional model checking algorithms (LTL and CTL model checking) and current approaches (bounded model checking, k-induction, CEGAR, property-driven reachability);
be able to read and write specifications in LTL and CTL;
be aware of potential applications and inherent limitations of model checking algorithms. - Syllabus
- Overview of the model checking area.
- Kripke structure, labelled transition system, LTL, CTL, Büchi automata.
- Automata-based LTL model checking.
- CTL model checking.
- Bounded model checking and k-induction.
- Reachability in pushdown systems.
- Abstraction and CEGAR.
- Property directed reachability.
- Literature
- CLARKE, E. M., Orna GRUMBERG, Doron PELED, Daniel KROENING and Helmut VEITH. Model checking. Second edition. Cambridge, Massachusetts: MIT Press, 2018, xx, 402. ISBN 9780262038836. info
- Handbook of model checking. Edited by E. M. Clarke - T. A. Henzinger - Helmut Veith - Roderick Bloem. Cham: Springer International Publishing AG, 2018, xxiv, 1210. ISBN 9783319105741. info
- Teaching methods
- lectures, seminars
- Assessment methods
- oral exam
- Language of instruction
- English
- Further Comments
- The course is taught annually.
The course is taught: every week.
IA169 Model Checking
Faculty of InformaticsSpring 2024
- Extent and Intensity
- 2/1/0. 3 credit(s) (plus extra credits for completion). Type of Completion: zk (examination).
- Teacher(s)
- prof. RNDr. Jan Strejček, Ph.D. (lecturer)
RNDr. Martin Jonáš, Ph.D. (seminar tutor) - Guaranteed by
- prof. RNDr. Jan Strejček, Ph.D.
Department of Computer Science – Faculty of Informatics
Supplier department: Department of Computer Science – Faculty of Informatics - Timetable
- Mon 19. 2. to Thu 9. 5. Thu 16:00–17:50 A318
- Timetable of Seminar Groups:
- Prerequisites
- 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: 12/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
- there are 33 fields of study the course is directly associated with, display
- Course objectives
- The student will understand the fundamental and currently used model checking algorithms and techniques (except those primarily designed for software). Further, the student will be able to read and write specifications in LTL and CTL, and use relevant formalisms like Büchi automata and binary decision diagrams.
- Learning outcomes
- Students will:
understand traditional model checking algorithms (LTL and CTL model checking) and current approaches (bounded model checking, k-induction, CEGAR, property-driven reachability);
be able to read and write specifications in LTL and CTL;
be aware of potential applications and inherent limitations of model checking algorithms. - Syllabus
- Overview of the model checking area.
- Kripke structure, labelled transition system, LTL, CTL, Büchi automata.
- Automata-based LTL model checking.
- CTL model checking.
- Bounded model checking and k-induction.
- Reachability in pushdown systems.
- Abstraction and CEGAR.
- Property directed reachability.
- Literature
- CLARKE, E. M., Orna GRUMBERG, Doron PELED, Daniel KROENING and Helmut VEITH. Model checking. Second edition. Cambridge, Massachusetts: MIT Press, 2018, xx, 402. ISBN 9780262038836. info
- Handbook of model checking. Edited by E. M. Clarke - T. A. Henzinger - Helmut Veith - Roderick Bloem. Cham: Springer International Publishing AG, 2018, xxiv, 1210. ISBN 9783319105741. info
- Teaching methods
- lectures, seminars
- Assessment methods
- oral exam
- Language of instruction
- English
- Further Comments
- Study Materials
The course is taught annually.
IA169 System Verification and Assurance
Faculty of InformaticsAutumn 2022
- 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)
doc. RNDr. Vojtěch Řehák, Ph.D. (seminar tutor)
Mgr. Pavol Žáčik (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 16:00–17:50 A217
- 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: 20/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
- there are 33 fields of study the course is directly associated with, display
- 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.
IA169 System Verification and Assurance
Faculty of InformaticsAutumn 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:
- 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
- there are 32 fields of study the course is directly associated with, display
- 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.
IA169 System Verification and Assurance
Faculty of InformaticsAutumn 2020
- Extent and Intensity
- 2/0/2. 4 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
- Teacher(s)
- 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)
RNDr. Marek Chalupa, Ph.D. (seminar tutor) - 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 16:00–17:50 A217
- Timetable of Seminar Groups:
IA169/02: Mon 10:00–11:50 A219, M. Chalupa, V. Řehák - Prerequisites
- (! 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 130 student(s).
Current registration and enrolment status: enrolled: 0/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
- there are 32 fields of study the course is directly associated with, display
- 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.
- 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. 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.
- Literature
- GRUMBERG, Orna, Doron A. PELED and E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
- Teaching methods
- lectures, seminars/labs, 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.
IA169 System Verification and Assurance
Faculty of InformaticsAutumn 2019
- Extent and Intensity
- 2/0/2. 4 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: k (colloquium).
- Teacher(s)
- 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)
RNDr. Marek Chalupa, Ph.D. (seminar tutor) - 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 16:00–17:50 A217
- Timetable of Seminar Groups:
IA169/02: Mon 12:00–13:50 A219, M. Chalupa, V. Řehák - Prerequisites
- (! 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 70 student(s).
Current registration and enrolment status: enrolled: 1/70, only registered: 0/70, only registered with preference (fields directly associated with the programme): 0/70 - fields of study / plans the course is directly associated with
- there are 32 fields of study the course is directly associated with, display
- 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.
- 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. 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.
- Literature
- GRUMBERG, Orna, Doron A. PELED and E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
- Teaching methods
- lectures, seminars/labs, 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.
IA169 System Verification and Assurance
Faculty of InformaticsSpring 2019
- 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).
- Teacher(s)
- 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)
RNDr. Marek Chalupa, Ph.D. (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 - Timetable
- 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 - Prerequisites
- (! 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: 0/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
- Information Technology Security (eng.) (programme FI, N-IN)
- Information Technology Security (programme FI, N-IN)
- 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.
- 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. 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
- English
- Follow-Up Courses
- Further Comments
- Study Materials
The course is taught annually.
IA169 System Verification and Assurance
Faculty of InformaticsSpring 2018
- 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).
- Teacher(s)
- 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)
RNDr. Marek Chalupa, Ph.D. (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 - Timetable
- Tue 12:00–13:50 A218
- Timetable of Seminar Groups:
IA169/02: Wed 14:00–15:50 A219, M. Chalupa, V. Řehák - Prerequisites
- (! 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: 0/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
- Information Technology Security (eng.) (programme FI, N-IN)
- Information Technology Security (programme FI, N-IN)
- 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.
- 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. 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
- English
- Follow-Up Courses
- Further Comments
- Study Materials
The course is taught annually.
IA169 System Verification and Assurance
Faculty of InformaticsSpring 2017
- 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).
- Teacher(s)
- 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)
RNDr. Marek Chalupa, Ph.D. (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 - Timetable
- Tue 12:00–13:50 B410
- Timetable of Seminar Groups:
IA169/02: Wed 18:00–19:50 A219, M. Chalupa - Prerequisites
- (! 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: 0/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
- Information Technology Security (eng.) (programme FI, N-IN)
- Information Technology Security (programme FI, N-IN)
- 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.
- 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. 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
- English
- Follow-Up Courses
- Further Comments
- Study Materials
The course is taught annually.
IA169 System Verification and Assurance
Faculty of InformaticsSpring 2016
- 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).
- Teacher(s)
- 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)
Dr. rer. nat. Achim Blumensath (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 - Timetable
- Tue 12:00–13:50 A218
- Timetable of Seminar Groups:
IA169/02: Fri 10:00–11:50 A219, A. Blumensath - Prerequisites
- (! 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: 0/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
- Information Technology Security (eng.) (programme FI, N-IN)
- Information Technology Security (programme FI, N-IN)
- 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.
- 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. 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
- English
- Follow-Up Courses
- Further Comments
- Study Materials
The course is taught annually.
IA169 System Verification and Assurance
Faculty of InformaticsSpring 2015
The course is not taught in Spring 2015
- Extent and Intensity
- 2/2/2. 6 credit(s) (plus extra credits for completion). Type of Completion: zk (examination).
- Teacher(s)
- prof. RNDr. Jiří Barnat, Ph.D. (lecturer)
prof. RNDr. Václav Matyáš, M.Sc., Ph.D. (lecturer) - 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 - Prerequisites
- User-level familiarity with Unix/Linux operating system. Basics of C programming. Basic astract math reasoning.
- Course Enrolment Limitations
- The course is offered to students of any study field.
The capacity limit for the course is 30 student(s).
Current registration and enrolment status: enrolled: 0/30, only registered: 0/30, only registered with preference (fields directly associated with the programme): 0/30 - Course objectives
- This course will provide the necessary theoretic background as well as 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.
- 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. 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
- English
- Follow-Up Courses
- Enrolment Statistics (Spring 2025, recent)