Speaker: Dr. Mirco Giacobbe (University of Oxford, UK)
Title: Neuro-symbolic Liveness Verification
Abstract: Liveness verification answers the question of whether a system always responds with desirable behavior or, dually, never gets stuck without responding at all. For dynamical systems, this relates to the stability question; for computer programs, it relates to the halting problem. I will talk about a novel method for constructing liveness proofs by learning witnesses (Lyapunov and ranking functions) from data using neural networks combined with symbolic reasoning. I will talk about how we apply this neuro-symbolic approach to the stability analysis of dynamical systems, to the termination analysis of Java programs, and to the almost-sure termination analysis of probabilistic programs.
When: Friday June 11th 2021 from 14.30 to 15.30
Where: Webex as follows:
Join from the meeting link
https://univaq.webex.com/univaq-en/j.php?MTID=m8cda8ceca3433cd9cea34cf6cd8749b1
Join by meeting number
Meeting number (access code): 137 780 9599
Meeting password: trZmujpx282
Tap to join from a mobile device (attendees only)
+39-069-974-8087,,1377809599## Italy Toll
+390230410440,,1377809599## Italy Toll 2
Join by phone
+39-069-974-8087 Italy Toll
390230410440 Italy Toll 2
Join from a video system or application
Dial 1377809599@univaq.webex.com
You can also dial 62.109.219.4 and enter your meeting number.