Non-Termination Proving: 100 Million LoC and Beyond

Julien Vanegue, Jules Villard, Peter O'Hearn +1

We report on our tool, Pulse Infinite, that uses proof techniques to show non-termination (divergence) in large programs. Pulse Infinite works compositionally and under-approximate…