Search for contacts, projects,
courses and publications

Computer Aided Verification

Description

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

In addition to theory lessons, the class will have labs that will involve using verification tools. We will illustrate automated verification using the USI HiFrog and UpProver projects (www.verify.inf.usi.ch) that use incremental SMT-based approach.

 

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

Asadi S.

Assistant

Additional information

Semester
Fall
Academic year
2021-2022
ECTS
6
Language
English
Education
Master of Science in Informatics, Elective course, 1st year
Master of Science in Informatics, Elective course, 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)