1 citations · 1 across the 4 of their papers we have counts for
Showing cs.LOShow all
3 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.LO2023★ 1 cited
Certifying C program correctness with respect to CH2O with VeriFast
Stefan Wils, Bart Jacobs
VeriFast is a powerful tool for verification of various correctness properties of C programs using symbolic execution. However, VeriFast itself has not been verified. We present a…
cs.LO2023
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…