Solving Verification Questions using Machine Learning

Abstract: Formal verification’s aim is that of deriving rigorous proofs for the correctness of systems and, traditionally, has mainly been tackled using automated reasoning methods. In this talk, I will argue that formal verification can be takled using statistical methods too. I will discuss the liveness verification question which, intuitively, is the question of whether a system always responds. For dynamical systems, this relates to the stability question; for computer programs, it is the halting problem. I will present a novel approach where neural networks are used to learn formal witnesses (ranking and Lyapunov functions) of liveness from data while ensuring formal soundness of these witness. I will show how we apply this method to the stability analysis of dynamical systems and to the termination analysis of probabilistic programs.

Bio: Mirco Giacobbe is a lecturer in computer science at the University of Birmingham. He was a postdoc at the University of Oxford under the supervision of Alessandro Abate and Daniel Kroening and completed his Phd at IST Austria under the supervision of Tom Henzinger. His research interests include reasoning methods for safe artificial intelligence and cyber-physical systems and machine learning methods for formal verification.

Link to the profile of Mirco Giacobbe