Guest Talk: Cristina David: Lessons learnt from using GNNs to estimate program termination

Thursday, October 12, 2023, 1pm

Location: RWTH Aachen University, Department of Computer Science - Ahornstr. 55, building E2, room 5053.2 (B-IT)

Speaker: Cristina David, University of Bristol, UK


​Termination analyses investigate the termination behaviour of programs in order to prevent a variety of program bugs (e.g. hanging programs, denial-of-service vulnerabilities). Usually, such analyses make use of formal methods and provide certificates of correctness in the form of ranking functions or recurrence sets. In this work, we move away from formal methods and embrace the stochastic nature of machine learning models. Instead of aiming for rigorous guarantees that can be interpreted by solvers, our objective is to provide an estimation of a program's termination behaviour and of the likely reason for nontermination (when applicable) that a programmer can use for debugging purposes.

In this talk, I will discuss our experience using Graph Neural Networks and semantic segmentation for this purpose, as well as the challenges we encountered and possible solutions.