Computer Aided Verification
People
Course director
Assistant
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 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.
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 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.
Teaching mode
In presence
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.
Bibliography
Education
- Master of Science in Artificial Intelligence, Lecture and Laboratory, Elective, 1st year
- Master of Science in Informatics, Lecture and Laboratory, Computer Systems, Elective, 1st year
- Master of Science in Informatics, Lecture and Laboratory, Computer Systems, Elective, 2nd year
- Master of Science in Informatics, Lecture and Laboratory, Software Development, Elective, 1st year
- Master of Science in Informatics, Lecture and Laboratory, Software Development, Elective, 2nd year
- Master of Science in Informatics, Lecture and Laboratory, Theory and Algorithms, Elective, 1st year
- Master of Science in Informatics, Lecture and Laboratory, Theory and Algorithms, Elective, 2nd year
- Master of Science in Informatics, Lecture and Laboratory, Programming languages, Elective, 1st year
- Master of Science in Informatics, Lecture and Laboratory, Programming languages, Elective, 2nd year
- PhD programme of the Faculty of Informatics, Lecture and Laboratory, Elective, 1st year (4.0 ECTS)