1 citations · 2 across the 7 of their papers we have counts for
9 papers
DeCo: A Core Calculus for Incremental Functional Programming with Generic Data Types
Timon Böhler, Tobias Reinhard, David Richter +1
Incrementalization speeds up computations by avoiding unnecessary recomputations and by efficiently reusing previous results. While domain-specific techniques achieve impressive sp…
Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds
Tobias Reinhard
In this dissertation we describe two contributions to the state of the art in reasoning about liveness and safety, respectively. Programs for multiprocessor machines commonly perfo…
Completeness Thresholds for Memory Safety: Unbounded Guarantees via Bounded Proofs (Extended Abstract)
Tobias Reinhard, Justus Fasse, Bart Jacobs
Bounded proofs are convenient to use due to the high degree of automation that exhaustive checking affords. However, they fall short of providing the robust assurances offered by u…
Completeness Thresholds for Memory Safety of Array Traversing Programs
Tobias Reinhard, Justus Fasse, Bart Jacobs
We report on intermediate results of -- to the best of our knowledge -- the first study of completeness thresholds for (partially) bounded memory safety proofs. Specifically, we co…
Completeness Thresholds for Memory Safety of Array Traversing Programs: Early Technical Report
Tobias Reinhard
In this early technical report on an ongoing project, we present -- to the best of our knowledge -- the first study of completeness thresholds for memory safety proofs. Specificall…
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit
Tobias Reinhard, Amin Timany, Bart Jacobs
Programs for multiprocessor machines commonly perform busy-waiting for synchronisation. In this paper, we make a first step towards proving termination of such programs. We approxi…