Computer Aided Verification

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 automated verification by Model Checking, and discuss the complementary techniques of automated abstraction and symbolic reasoning, which advanced it to the widespread use in industry. We will look into examples verifying correctness of various applications such as smart contracts and general purpose software.

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 and security 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.

In presence

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.