Page Not Found
Page not found. Your pixels are in another canvas.
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
About me
About me
Page not in menu
This is a page not in th emain menu
Resources for Students
Resources for students
Posts
Future Blog Post
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
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
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
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
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
Portfolio item number 1
Short description of portfolio item number 1
Portfolio item number 2
Short description of portfolio item number 2
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
[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
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
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 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]
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]
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]
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: 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]
[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]
talks
[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.
Ghost Signals: Verifying Termination of Busy Waiting
Published:
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.
[Invited Talk] Completeness Thresholds for Memory Safety: Unbounded Guarantees Via Bounded Proofs
Published:
In this invited talk, we present the first notion of completeness thresholds for memory safety proofs. They allow us to reduce unbounded memory safety proofs to bounded ones.
[Poster Presentation] Completeness Thresholds for Memory Safety: Unbounded Guarantees Via Bounded Proofs
Published:
With this poster, we present the first notion of completeness thresholds for program verification. They allow us to reduce unbounded memory safety proofs to bounded ones.
[Invited Talk] Completeness Thresholds for Memory Safety: Unbounded Guarantees Via Bounded Proofs
Published:
In this invited talk, we present the first notion of completeness thresholds for memory safety proofs. They allow us to reduce unbounded memory safety proofs to bounded ones.
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.