A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit


In this talk we present our work on verifying termination of programs where some threads eventually abruptly terminate the program, and other threads busy-wait for this to happen. Further, we outline our plans to generalize this approach to verify termination of busy-waiting for arbitrary events.