Model checking as Machine Learning

DISI Seminar 2024
11 luglio 2024
Orario di inizio 
Polo Ferrari 2 - Via Sommarive 9, Povo (Trento)
aula B108
Organizzato da: 
Dipartimento di Ingegneria e Scienza dell'Informazione
Comunità universitaria
Ingresso libero
prof. Marco Roveri
Mirco Giacobbe, University of Birmingham


Model checking aims to derive rigorous proofs for the correctness of systems and has traditionally relied on symbolic reasoning methods.
In this talk, I will argue that model checking can also be effectively addressed using machine learning too. I will present a realm of approaches for formal verification that leverage neural networks to represent correctness certificates of systems, known as "neural certificates." This approach trains certificates from synthetic executions of the system and then validates them using symbolic reasoning techniques. Building upon the observation that checking a correctness certificate is much simpler than finding one, and that neural networks are an appropriate representation for such certificates, this results in a machine learning approach to model checking that is entirely unsupervised, formally sound, and practically effective. I will demonstrate the principles and experimental results of this approach in safety assurance of software, probabilistic systems, and control.

About the speaker

Mirco Giacobbe is an Assistant Professor at the University of Birmingham. He previously held research positions at the University of Oxford and Fondazione Bruno Kessler. He obtained his PhD at the Institute and Science and Technology Austria and studied at the University of Trento and RWTH Aachen. His research interests lie between formal me­thods and artificial intelligence, where he develops automatic techniques to assure that algorithmic systems are safe and trustworthy.