Posts by Collection

Portfolio item number 1

Short description of portfolio item number 1

Portfolio item number 2

Short description of portfolio item number 2

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

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]

[Pre-Print] A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit

Accepted at 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://arxiv.org/abs/2010.07800
[Bibtex]

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

Published in arxiv.org, 2020

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. 2020. https://arxiv.org/abs/2010.11762
[Bibtex]

[Poster Presentation] Type-Level Latency Tracking with Placement Types

Published:

We propose a language design which makes latency and locations explicit and extracts static type-level bounds for a computation’s runtime latency.

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

Published:

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.

Teaching experience 1

Undergraduate course, University 1, Department, 2014

This is a description of a teaching experience. You can use markdown like any other post.

Teaching experience 2

Workshop, University 1, Department, 2015

This is a description of a teaching experience. You can use markdown like any other post.