Ricerca di contatti, progetti,
corsi e pubblicazioni

Computer Aided Verification

Persone

Sharygina N.

Docente titolare del corso

Britikov K.

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