Model checking as Machine Learning

DISI Seminar 2024
11 July 2024
Start time 
11:00 am
Polo Ferrari 2 - Via Sommarive 9, Povo (Trento)
room B108
Department of Information Engineering and Computer Science
Target audience: 
University community
Contact person: 
prof. Marco Roveri
Contact details:
Mirko 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.