104 citations · 478 across the 35 of their papers we have counts for
41 papers
Certifying C program correctness with respect to CompCert 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…
From Multisets over Distributions to Distributions over Multisets
Bart Jacobs
A well-known challenge in the semantics of programming languages is how to combine non-determinism and probability. At a technical level, the problem arises from the fact that ther…
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…
Ghost Signals: Verifying Termination of Busy-Waiting (Extended Version)
Tobias Reinhard, Bart Jacobs
Programs for multiprocessor machines commonly perform busy waiting for synchronization. We propose the first separation logic for modularly verifying termination of such programs u…
A Separation Logic to Verify Termination of Busy-Waiting for Abrupt Program Exit: Technical Report
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…
Steps and Traces
Jurriaan Rot, Bart Jacobs, Paul Levy
In the theory of coalgebras, trace semantics can be defined in various distinct ways, including through algebraic logics, the Kleisli category of a monad or its Eilenberg-Moore cat…