Computer Aided Verification
Persone
Docente titolare del corso
Assistente
Descrizione
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.
Obiettivi
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.
Modalità di insegnamento
In presenza
Impostazione pedagogico-didattica
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.
Modalità d’esame
There will be a written final exam covering the material presented in class.
Bibliografia
Offerta formativa
- Master of Science in Informatics, Lezione, Computer Systems, A scelta, 1° anno
- Master of Science in Informatics, Lezione, Computer Systems, A scelta, 2° anno
- Master of Science in Informatics, Lezione, Software Development, A scelta, 1° anno
- Master of Science in Informatics, Lezione, Software Development, A scelta, 2° anno
- Master of Science in Informatics, Lezione, Theory and Algorithms, A scelta, 1° anno
- Master of Science in Informatics, Lezione, Theory and Algorithms, A scelta, 2° anno
- Master of Science in Informatics, Lezione, Programming languages, A scelta, 1° anno
- Master of Science in Informatics, Lezione, Programming languages, A scelta, 2° anno
- Dottorato in Scienze informatiche, Lezione, A scelta, 1° anno (4.0 ECTS)