Guest Talk: Mirco Giacobbe: Neural Termination Analysis

Wednesday, May 12, 2021, 10:30am

Meeting-ID: 996 6919 8425, Passcode: 878733

Speaker: Mirco Giacobbe (University of Oxford, UK)



Termination analysis answers the question of whether a program always responds or, dually, never gets stuck in an infinite loop. This is unsolvable in general, yet tools that work in practice have been developed in industry and academia. The major existing methods construct termination proofs via symbolic reasoning from the source code. I will talk about a novel method for learning termination proofs from execution traces. We let neural networks fit termination witnesses over execution traces and then use satisfiability modulo theories for checking whether they generalise to all possible executions. Thanks to the ability of neural networks to generalise well, neural termination analysis succeeds over a wide variety of programs. Moreover, it is extremely simple to implement. I will talk about how we apply neural termination analysis to the termination analysis of Java programs that use data structures, to the almost-sure termination analysis of probabilistic programs, and to the stability analysis of cyber-physical systems.