1 citations · 3 across the 5 of their papers we have counts for
5 papers
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…
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…
Verification of C++ Programs with VeriFast
Niels Mommen, Bart Jacobs
VeriFast is a prototype tool based on separation logic for modular verification of C and Java programs. We are in the process of adding support for C++. In this report, we describe…
Modular Formal Verification of Rust Programs with Unsafe Blocks
Nima Rahimi Foroushaani, Bart Jacobs
Rust is a modern systems programming language whose type system guarantees memory safety. For the sake of expressivity and performance it allows programmers to relax typing rules t…