Sitemap

A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.

Pages

Posts

Future Blog Post

less than 1 minute read

Published:

This post will show up by default. To disable scheduling of future posts, edit config.yml and set future: false.

Blog Post number 4

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

Blog Post number 3

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

Blog Post number 2

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

Blog Post number 1

less than 1 minute read

Published:

This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.

portfolio

publications

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]

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]

[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]

talks

teaching

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.