1 citations · 1 across the 4 of their papers we have counts for
4 papers
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…
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…
Verifying C++ Dynamic Binding
Niels Mommen, Bart Jacobs
We propose an approach for modular verification of programs written in an object-oriented language where, like in C++, the same virtual method call is bound to different methods at…
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…