Showing cs.LOShow all
2 papers · 1 filter
cs.LO2023
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…
cs.LO2022
Modular termination verification with a higher-order concurrent separation logic (Intermediate report)
Justus Fasse, Bart Jacobs
We report on intermediate results of our research on reasoning about liveness properties in addition to deep correctness properties for an imperative, concurrent programming langua…