@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}
}