IV113 Introduction to Validation and Verification

Faculty of Informatics
Autumn 2017
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 C525
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
there are 47 fields of study the course is directly associated with, display
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
The course is also listed under the following terms Autumn 2007, Autumn 2008, Autumn 2009, Autumn 2010, Autumn 2011, Autumn 2012, Autumn 2013, Autumn 2014, Autumn 2015, Autumn 2016, Autumn 2018.
  • Enrolment Statistics (Autumn 2017, recent)
  • Permalink: https://is.muni.cz/course/fi/autumn2017/IV113