Publications

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

Accepted at CAV, 2021

We propose the first separation logic to modularly verify termination of busy-waiting. Our logic requires the proof author to associate a so-called ghost signal with each busy-waiting loop and allows such loops to iterate while their corresponding signal is not set. By using conventional shared state invariants to associate the state of ghost signals with the state of data structures, programs busy-waiting for arbitrary conditions over arbitrary data structures can be verified.

Recommended citation: Tobias Reinhard and Bart Jacobs. Ghost Signals: Verifying Termination of Busy-Waiting (Extended Version). 2021. https://arxiv.org/abs/2010.11762
[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