Course Details for A.Y. 2015/2016

Course Objectives

Il corso si propone di fornire una preparazione sulle tecniche di verifica formale, sia da un punto di vista teorico che pratico. Nella prima parte del corso verranno illustrati diversi strumenti formali utilizzati per la modellazione di sistemi e di proprietà. Nella seconda parte verrà approfondita l'applicazione pratica di tali strumenti formali attraverso l'utilizzo di diversi model checkers per la validazione di casi di studio reali. Infine verranno affrontati aspetti avanzati in particolare nell'ambito della sintesi automatica di sistemi reattivi.

Course Content

• Scope of formal verification
• Temporal logic, Kripke structures, timed automata, hybrid automata
• Reachability, Safety, Liveness, Fairness
• Modeling of protocols, hyrid systems and control systems
• Symbolic Model Checking: SMV, HyTech. Explicit Model Checking: SPIN, Murphi
• Model-checking techniques for the automatic synthesis of controllers and plans

Assessment Methods and Criteria

La prova di esame consiste in una prova progettuale, una prova scritta sulle due parti del corso e una prova orale sulle due parti del corso.

Textbooks

• B. Bérard et al., Systems and Software Verification , Springer. http://www.springer.com/computer/programming/book/978-3-540-41523-7   

Internet Resources

Course page updates

• A.Y. 2010/2011
• A.Y. 2013/2014
• A.Y. 2014/2015
• A.Y. 2015/2016
• A.Y. 2016/2017
• A.Y. 2017/2018
• A.Y. 2018/2019