Alma universitas studiorum parmensis A.D. 962 - Università di Parma
EUGreen - European University Alliance for sustainability

Event description

Automated reasoning has recently found important industrial applications in the fields of security and privacy, as well as formal verification. This talk offers an introduction to SMT (Satisfiability Modulo Theories) solving, a relevant branch of automated reasoning, and its use in software verification. We will explain the basic concepts behind the inner workings of SMT solvers, and provide a brief guide on how to use them, focusing on Microsoft Research’s Z3 Theorem Prover. Finally, we will show how SMT solvers can be employed to automatically verify the correctness of  software programs.
 

Access mode

Live: Ingresso libero fino esaurimento posti

It's part of

Campus - Plesso di Matematica
Ingresso libero fino esaurimento posti
Modified on