Skip to main content

Solving Verification Questions using Machine Learning

Save to calendar

Oct 26

Date and time: 26 October 2021, 15:00-16:00 CEST (UTC +2)
Speaker: Mirco Giacobbe, University of Birmingham
Title: Solving Verification Questions using Machine Learning

Zoom: https://kth-se.zoom.us/j/69560887455
Meeting ID: 695 6088 7455
Password: 755440

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