12 citations · 31 across the 14 of their papers we have counts for
14 papers
Nondeterminism and Guarded Commands
Krzysztof R. Apt, Ernst-Rüdiger Olderog
The purpose of this paper is to discuss the relevance of nondeterminism in computer science, with a special emphasis on Dijkstra's guarded commands language.
Concurrent Hyperproperties
Bernd Finkbeiner, Ernst-Rüdiger Olderog
Trace properties, which are sets of execution traces, are often used to analyze systems, but their expressiveness is limited. Clarkson and Schneider defined hyperproperties as a ge…
Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory (Full Version)
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch +1
In the synthesis of distributed systems, we automate the development of distributed programs and hardware by automatically deriving correct implementations from formal specificatio…
Model Checking Branching Properties on Petri Nets with Transits (Full Version)
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch +1
To model check concurrent systems, it is convenient to distinguish between the data flow and the control. Correctness is specified on the level of data flow whereas the system is c…
AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL (Full Version)
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch +1
The correctness of networks is often described in terms of the individual data flow of components instead of their global behavior. In software-defined networks, it is far more con…
Model Checking Data Flows in Concurrent Network Updates (Full Version)
Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch +1
We present a model checking approach for the verification of data flow correctness in networks during concurrent updates of the network configuration. This verification problem is…