30 citations · 87 across the 9 of their papers we have counts for
10 papers
Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic
Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers
Message passing is a useful abstraction for implementing concurrent programs. For real-world systems, however, it is often combined with other programming and concurrency paradigms…
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
Dan Frumin, Robbert Krebbers, Lars Birkedal
We present a new version of ReLoC: a relational separation logic for proving refinements of programs with higher-order state, fine-grained concurrency, polymorphism and recursive t…
Compositional Non-Interference for Fine-Grained Concurrent Programs
Dan Frumin, Robbert Krebbers, Lars Birkedal
Non-interference is a program property that ensures the absence of information leaks. In the context of programming languages, there exist two common approaches for establishing no…
A benchmark for C program verification
Marko van Eekelen, Daniil Frumin, Herman Geuvers +7
We present twenty-five C programs, as a benchmark for C program verification using formal methods. This benchmark can be used for system demonstration, for comparison of verificati…
A Formal C Memory Model for Separation Logic
Robbert Krebbers
The core of a formal semantics of an imperative programming language is a memory model that describes the behavior of operations on the memory. Defining a memory model that matches…
A call-by-value lambda-calculus with lists and control
Robbert Krebbers
Calculi with control operators have been studied to reason about control in programming languages and to interpret the computational content of classical proofs. To make these calc…