Publications

[Pre-Print] Ghost Signals: Verifying Termination of Busy-Waiting

Published in , 2021

We propose a separation logic using so-called ghost signals to modularly verify termination of busy-waiting programs under fair scheduling. Intuitively spoken, ghost signals lift the runtime concept of wait-notify synchronization to the verification level and allow a thread to busy-wait for an event $X$ while another thread promises to trigger $X$.

Recommended citation: Tobias Reinhard and Bart Jacobs. Ghost Signals: Verifying Termination of Busy-Waiting. 2021. https://drive.google.com/file/d/1oCCyINFeHxo4HPIadRTCj1u6i2kQPZB_/view
[Bibtex]

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

Published in FTfJP, 2020

We propose a separation logic for modularly verifying termination of programs where some threads eventually abruptly terminate the program, and other threads busy-wait for this to happen. This work is a first step towards verifying termination of programs involving busy-waiting for arbitrary events.

Recommended citation: Tobias Reinhard, Amin Timany, and Bart Jacobs. A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit. Accepted at Formal Techniques for Java-like Programs (2020). https://dl.acm.org/doi/10.1145/3427761.3428345
[Bibtex]

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

Published in arxiv.org, 2020

We propose a separation logic for modularly verifying termination of programs where some threads eventually abruptly terminate the program, and other threads busy-wait for this to happen. This work is a first step towards verifying termination of programs involving busy-waiting for arbitrary events.

Recommended citation: Tobias Reinhard, Amin Timany, and Bart Jacobs. A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report. 2020. https://arxiv.org/abs/2007.10215
[Bibtex]

Static Latency Tracking with Placement Types

Published in FTfJP, 2018

We present a preliminary investigation of a type system that tracks latency and makes the cost of remote calls explicit, raising developers’ awareness of communication overhead.

Recommended citation: Pascal Weisenburger, Tobias Reinhard, and Guido Salvaneschi. 2018. Static Latency Tracking with Placement Types. In Companion Proceedings for the ISSTA/ECOOP 2018 Workshops (FTfJP’18). July 16–21, 2018, Amsterdam, Netherlands. ACM, New York, NY, USA, 34–36. http://doi.org/10.1145/3236454.3236486 https://dl.acm.org/doi/10.1145/3236454.3236486