A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit
Date:
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.
- Presentation
- [Paper] accepted at FTfJP 2020
- Technical Report