Computer Aided Verification
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.
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.
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.
There will be a written final exam covering the material presented in class.
- 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)
- 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)