Dear all,

on Wednesday, May 12, at 10:30 am, Mirco Giacobbe from the University of Oxford will give a talk on his recent work of applying neural networks to perform termination analysis.

Wednesday, 12.05.2021, 10:30 am
https://rwth.zoom.us/j/99669198425?pwd=NTNzTGNnYjNrQUc0ZDFTTVdiWjY4UT09
Meeting-ID: 996 6919 8425, Passcode: 878733

Everybody is welcome!

Best regards

Helen Bolke-Hermanns

-----------------------------------------------------------------------------------------

Mirco Giacobbe (University of Oxford, UK): Neural Termination Analysis

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.

More information: https://www.unravel.rwth-aachen.de/go/id/nyoee