Search for contacts, projects,
courses and publications

Computer Aided Verification

Description

This course will not be offered in the academic year 2020/21

*****************************

 

COURSE OBJECTIVES

This is a course on automated verification techniques which is a graduate level introduction to the theory and practice of formal verification as an aid in the analysis of the correctness of programs. Though formal analysis requires understanding of many theoretical issues, the focus of this course will be on using practical verification tools to analyse industrial examples.

 

COURSE DESCRIPTION
Logical errors in programs can be costly, even life threatening. This course we will cover foundational concepts, and tools built on them, for finding and preventing such errors. We will cover some of the most prominent ideas in the Turing award winning technology of Model Checking, and discuss the complementary techniques of automated abstraction and symbolic reasoning, which advanced automated verification to the practical use in industry.

 

LEARNING METHODS
We will cover just enough theory to use the CAV tools effectively and understand the examples. In addition to lectures, the class will have labs that will involve using verification tools.

 

EXAMINATION INFORMATION
There will be a written final exam covering the material presented in class.

 

REFERENCES

  • Principles of Model Checking, C. Baier, and J. Katoen, MIT Press, 2008, ISBN 978-0-262-02649-9 (main reference book)
  • Model Checking, E. Clarke, O. Grumberg, and D. Peled, MIT Press, 2000, ISBN 0-262-03270-8 (recommended)

People

 

Sharygina N.

Course director

Additional information

Semester
Fall
Academic year
2020-2021
ECTS
6
Language
English
Education
Master of Science in Informatics, Elective course, Lecture, 1st year
Master of Science in Informatics, Elective course, Lecture, 2nd year
PhD programme of the Faculty of Informatics, Elective course, Lecture, 1st year (4 ECTS)
PhD programme of the Faculty of Informatics, Elective course, Lecture, 2nd year (4 ECTS)