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.