Talks and Presentations

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

July 23, 2020

Talk, FTfJP 2020, online (virtual workshop)

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.