Publications

[Dissertation] Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds

Published in KU Leuven, 2024

In this dissertation we describe two contributions to the state of the art in reasoning about liveness and safety: Ghost signals for and completeness thresholds.

Recommended citation: Tobias Reinhard. 2024. Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds. https://lirias.kuleuven.be/4140343&lang=en
[Bibtex]

Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs (Extended Abstract)

Published in arXiv, 2023

Bounded proofs are easy to automate, yet lack the guarantees of unbounded proofs. We illustrate how completeness thresholds allow us to bridge this gap by only considering a few specific inputs.

Recommended citation: Tobias Reinhard, Justus Fasse and Bart Jacobs. 2023. Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs (Extended Abstract). arXiv:2309.09731 https://arxiv.org/abs/2309.09731
[Bibtex]

Completeness Thresholds for Memory Safety of Array Traversing Programs

Published in SOAP, 2023

We report on intermediate results of the first study of completeness thresholds for bounded memory safety proofs. These completeness thresholds allow us to reduce unbounded proofs to bounded ones.

Recommended citation: Tobias Reinhard, Justus Fasse and Bart Jacobs. 2023. Completeness Thresholds for Memory Safety of Array Traversing Programs. In Proceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis https://dl.acm.org/doi/abs/10.1145/3589250.3596143
[Bibtex]

Completeness Thresholds for Memory Safety of Array Traversing Programs: Early Technical Report

Published in arxiv.org, 2023

This technical report provides an overview of an ongoing project: The first study of completeness thresholds for bounded memory safety proofs. These completeness thresholds allow us to reduce unbounded proofs to bounded ones.

Recommended citation: Tobias Reinhard. 2023. Completeness Thresholds for Memory Safety of Array Traversing Programs: Early Technical Report. arXiv:2211.11885 https://arxiv.org/abs/2211.11885
[Bibtex]

Ghost Signals: Verifying Termination of Busy Waiting

Published in CAV, 2021

We propose the first separation logic to modularly verify termination of busy-waiting. We achieve this by introducing a novel type of ghost resource, called ghost signals.

Recommended citation: Tobias Reinhard and Bart Jacobs. 2021. Ghost Signals: Verifying Termination of Busy-Waiting (Extended Version). https://link.springer.com/chapter/10.1007/978-3-030-81688-9_2
[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 threads busy wait for abrupt termination. 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. 2020. A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit. Accepted at Formal Techniques for Java-like Programs. 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

This technical report describes a separation logic to modularly verify termination of programs where threads busy wait for abrupt termination. This is a first step towards verifying termination of programs involving busy waiting for arbitrary events.

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

A Core Calculus for Static Latency Tracking with Placement Types

Published in Student Research Competition @ POPL 2019, 2019

This core calculus implements a novel language design which supports to static reasoning about latency. It makes latency and locations explicit and extracts static type-level bounds for a computation’s runtime latency.

Recommended citation: Tobias Reinhard. 2019. A Type System for Static Latency Tracking. Student Research Competition @ POPL https://raw.githubusercontent.com/tobireinhard/Publications/master/SRC_papers/POPL19-SRC--CoreCalculusStaticLatencyTracking.pdf

[Master Thesis] A Type System for Static Latency Tracking

Published in TU Darmstadt, 2018

We propose a novel language design that supports static reasoning about runtime latency. It makes latency and locations explicit and extracts static type-level bounds for a computation’s runtime latency.

Recommended citation: Tobias Reinhard. 2018. A Type System for Static Latency Tracking. https://raw.githubusercontent.com/tobireinhard/Publications/master/theses/MasterThesis--Tobias_Reinhard--StaticLatencyTracking.pdf

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