7 citations · 15 across the 10 of their papers we have counts for
10 papers
Realizability in Semantics-Guided Synthesis Done Eagerly
Roland Meyer, Jakob Tepe, Sebastian Wolff
We present realizability and realization logic, two program logics that jointly address the problem of finding solutions in semantics-guided synthesis. What is new is that we proce…
Context-Aware Separation Logic
Roland Meyer, Thomas Wies, Sebastian Wolff
Separation logic is often praised for its ability to closely mimic the locality of state updates when reasoning about them at the level of assertions. The prover only needs to conc…
Make flows small again: revisiting the flow framework
Roland Meyer, Thomas Wies, Sebastian Wolff
We present a new flow framework for separation logic reasoning about programs that manipulate general graphs. The framework overcomes problems in earlier developments: it is based…
Embedding Hindsight Reasoning in Separation Logic
Roland Meyer, Thomas Wies, Sebastian Wolff
Proving linearizability of concurrent data structures remains a key challenge for verification. We present temporal interpolation as a new proof principle to conduct such proofs us…
Model-based Fault Classification for Automotive Software
Mike Becker, Roland Meyer, Tobias Runge +3
Intensive testing using model-based approaches is the standard way of demonstrating the correctness of automotive software. Unfortunately, state-of-the-art techniques leave a cruci…
A Concurrent Program Logic with a Future and History
Roland Meyer, Thomas Wies, Sebastian Wolff
Verifying fine-grained optimistic concurrent programs remains an open problem. Modern program logics provide abstraction mechanisms and compositional reasoning principles to deal w…
Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation
Roland Meyer, Sebastian Wolff
We consider the verification of lock-free data structures that manually manage their memory with the help of a safe memory reclamation (SMR) algorithm. Our first contribution is a…
Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
Roland Meyer, Sebastian Wolff
Verification of concurrent data structures is one of the most challenging tasks in software verification. The topic has received considerable attention over the course of the last…
Effect Summaries for Thread-Modular Analysis
Lukáš Holík, Roland Meyer, Tomáš Vojnar +1
We propose a novel guess-and-check principle to increase the efficiency of thread-modular verification of lock-free data structures. We build on a heuristic that guesses candidates…
Pointer Race Freedom
Frédéric Haziza, Lukáš Holík, Roland Meyer +1
We propose a novel notion of pointer race for concurrent programs manipulating a shared heap. A pointer race is an access to a memory address which was freed, and it is out of the…