@inproceedings{Reinhard2020AbruptExit, author = {Reinhard, Tobias and Timany, Amin and Jacobs, Bart}, title = {A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit}, year = {2020}, isbn = {9781450381864}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3427761.3428345}, doi = {10.1145/3427761.3428345}, abstract = {Programs for multiprocessor machines commonly perform busy-waiting for synchronisation. In this paper, we make a first step towards proving termination of such programs. We approximate (i) arbitrary waitable events by abrupt program termination and (ii) busy-waiting for events by busy-waiting to be abruptly terminated. We propose a separation logic for modularly verifying termination (under fair scheduling) of programs where some threads eventually abruptly terminate the program, and other threads busy-wait for this to happen.}, booktitle = {Proceedings of the 22nd ACM SIGPLAN International Workshop on Formal Techniques for Java-Like Programs}, pages = {26–32}, numpages = {7}, keywords = {Separation Logic, Termination, Busy-Waiting}, location = {Virtual, USA}, series = {FTfJP 2020} } @article{Reinhard2020AbruptExitTR, title={A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report}, author={Tobias Reinhard and Amin Timany and Bart Jacobs}, year={2020}, url={https://arxiv.org/abs/2007.10215}, eprint={2007.10215}, archivePrefix={arXiv}, primaryClass={cs.LO} }