14 citations · 48 across the 26 of their papers we have counts for
35 papers
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…
Urgency Annotations for Alternating Choices
Eren Keskin, Roland Meyer, Sören van der Wall
We propose urgency programs, a new programming model with support for alternation, imperfect information, and recursion. The novelty are urgency annotations that decorate the (ange…
Separability and Non-Determinizability of WSTS
Wojciech Czerwiński, Eren Keskin, Sławomir Lasota +4
We study the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that every pair of disjoint WSTS langu…
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…
Regular Separability in Büchi VASS
Pascal Baumann, Roland Meyer, Georg Zetzsche
We study the (-)regular separability problem for Büchi VASS languages: Given two Büchi VASS with languages and , check whether there is a regular language that fully…
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…