FI:IV113 Validation and Verification - Course Information
IV113 Introduction to Validation and Verification
Faculty of InformaticsAutumn 2018
- Extent and Intensity
- 2/0/0. 2 credit(s) (plus extra credits for completion). Recommended Type of Completion: zk (examination). Other types of completion: z (credit).
- Teacher(s)
- prof. RNDr. Jiří Barnat, Ph.D. (lecturer)
- Guaranteed by
- prof. RNDr. Mojmír Křetínský, CSc.
Department of Computer Science – Faculty of Informatics
Contact Person: prof. RNDr. Jiří Barnat, Ph.D.
Supplier department: Department of Computer Science – Faculty of Informatics - Timetable
- Wed 16:00–17:50 B411
- Prerequisites (in Czech)
- (! IA169 System Verif. and Assurance ) && (!NOW( 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
- Applied Informatics (programme FI, B-AP)
- Applied Informatics (programme FI, N-AP)
- Information Technology Security (eng.) (programme FI, N-IN)
- Information Technology Security (programme FI, N-IN)
- Bioinformatics (programme FI, B-AP)
- Bioinformatics (programme FI, N-AP)
- Information Systems (programme FI, N-IN)
- Informatics with another discipline (programme FI, B-BI)
- Informatics with another discipline (programme FI, B-EB)
- Informatics with another discipline (programme FI, B-FY)
- Informatics with another discipline (programme FI, B-GE)
- Informatics with another discipline (programme FI, B-GK)
- Informatics with another discipline (programme FI, B-CH)
- Informatics with another discipline (programme FI, B-IO)
- Informatics with another discipline (programme FI, B-MA)
- Informatics with another discipline (programme FI, B-SO)
- Informatics with another discipline (programme FI, B-TV)
- Informatics (eng.) (programme FI, D-IN4)
- Informatics (programme FI, B-IN)
- Informatics (programme FI, D-IN4)
- Informatics (programme FI, M-IN)
- Informatics (programme FI, N-IN)
- Mathematical Informatics (programme FI, B-IN)
- Parallel and Distributed Systems (programme FI, B-IN)
- Parallel and Distributed Systems (programme FI, N-IN)
- Computer Graphics and Image Processing (programme FI, B-IN)
- Computer Graphics (programme FI, N-IN)
- Computer Networks and Communication (programme FI, B-IN)
- Computer Networks and Communication (programme FI, N-IN)
- Computer Systems and Technologies (eng.) (programme FI, D-IN4)
- Computer Systems and Technologies (programme FI, D-IN4)
- Computer Systems and Data Processing (programme FI, B-IN)
- Computer Systems (programme FI, N-IN)
- Embedded Systems (eng.) (programme FI, N-IN)
- Programmable Technical Structures (programme FI, B-IN)
- Embedded Systems (programme FI, N-IN)
- Service Science, Management and Engineering (eng.) (programme FI, N-AP)
- Service Science, Management and Engineering (programme FI, N-AP)
- Social Informatics (programme FI, B-AP)
- Theoretical Informatics (programme FI, N-IN)
- Upper Secondary School Teacher Training in Informatics (programme FI, M-SS)
- Upper Secondary School Teacher Training in Informatics (programme FI, M-TV)
- Upper Secondary School Teacher Training in Informatics (programme FI, N-SS) (2)
- Artificial Intelligence and Natural Language Processing (programme FI, B-IN)
- Artificial Intelligence and Natural Language Processing (programme FI, N-IN)
- Image Processing (programme FI, N-AP)
- Course objectives
- The goal of this course is to get students oriented in the basic approaches to validation and verification of computer programs.
- Learning outcomes
- On successful completion of the course, students should be able to decide about validity of methods used to ensure the quality of a software project, should be able to formulate desired properties of a system in a temporal logic, should understand the way a model checker can be used to verify the temporal properties, and should be able to explain the principles the model checking tools build on.
- Syllabus
- Introduction to techniques of validation and verification. Testing missions. Strategy of testing, The oracle problem. Domain-based testing. Regression testing. Symbolic execution. Deductive verification. LTL model checking. CTL model checking. Techniques for state space reduction. Bounded model checking. Introduction to program analysis.
- Literature
- GRUMBERG, Orna, Doron A. PELED and E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708. info
- http://www.testingeducation.org/BBST/index.html
- BAIER, Christel and Joost-Pieter KATOEN. Principles of model checking. Cambridge, Mass.: MIT Press, 2008, xvii, 975. ISBN 9780262026499. info
- Teaching methods
- Lectures, homeworks.
- Assessment methods
- The course is completed with oral exam on all contents presented during the lectures. Personal participation at classes is not required. Obligatory homeworks if aspiring to be graded with A, voluntary otherwise.
- Language of instruction
- Czech
- Follow-Up Courses
- Further Comments
- Study Materials
The course is taught annually. - Teacher's information
- http://www.fi.muni.cz/~xbarnat/IV113/index.html
- Enrolment Statistics (recent)
- Permalink: https://is.muni.cz/course/fi/autumn2018/IV113