Formal verification plays an important role in the development cycle of several classes of software and systems (in particular the safety-critical ones) and also represents a useful tool for the researcher who wants, for example, prove the correctness of new protocols and algorithms. The course aims at illustrating the main formal verification techniques, with particular reference to those for concurrent and distributed software and systems. The course will address this topic mainly from the user point of view, giving the fundamental elements needed for understanding the potentiality and limitations of the various techniques. For this reason, particular emphasis will be given to the tools that implement or support the various techniques.

Programming skills and general knowledge about computer engineering as provided by a Master in Computer Engineering

1. Formal methods and their role in software and system lifecycles: classification and characterization of formal methods, their applications, their integration in lifecycles, standard examples. 2. Formal verification techniques: temporal logics, theorem proving, model checking, satisfiability modulo theories (SMT), abstraction techniques 3. Formal verification in practice: general-purpose verification tools example (Spin). 4. Examples of verification techniques and tools for special domains: source code verification, formal verification and synthesis of network configurations.

Modalità mista

Presentazione report scritto - Test a risposta multipla

P.D.2-2 - Maggio