Search for contacts, projects,
courses and publications

Computer Aided Verification

People

Sharygina N.

Course director

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)

Education