Document

**Published in:** LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)

Reactive synthesis automatically derives a strategy that satisfies a given specification. However, requiring a strategy to meet the specification in every situation is, in many cases, too hard of a requirement. Particularly in compositional synthesis of distributed systems, individual winning strategies for the processes often do not exist. Remorsefree dominance, a weaker notion than winning, accounts for such situations: dominant strategies are only required to be as good as any alternative strategy, i.e. , they are allowed to violate the specification if no other strategy would have satisfied it in the same situation. The composition of dominant strategies is only guaranteed to be dominant for safety properties, though; preventing the use of dominance in compositional synthesis for liveness specifications. Yet, safety properties are often not expressive enough. In this paper, we thus introduce a new winning condition for strategies, called delay-dominance, that overcomes this weakness of remorsefree dominance: we show that it is compositional for many safety and liveness specifications, enabling a compositional synthesis algorithm based on delay-dominance for general specifications. Furthermore, we introduce an automaton construction for recognizing delay-dominant strategies and prove its soundness and completeness. The resulting automaton is of single-exponential size in the squared length of the specification and can immediately be used for safraless synthesis procedures. Thus, synthesis of delay-dominant strategies is, as synthesis of winning strategies, in 2EXPTIME.

Bernd Finkbeiner and Noemi Passing. Synthesizing Dominant Strategies for Liveness. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 37:1-37:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:LIPIcs.FSTTCS.2022.37, author = {Finkbeiner, Bernd and Passing, Noemi}, title = {{Synthesizing Dominant Strategies for Liveness}}, booktitle = {42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)}, pages = {37:1--37:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-261-7}, ISSN = {1868-8969}, year = {2022}, volume = {250}, editor = {Dawar, Anuj and Guruswami, Venkatesan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.37}, URN = {urn:nbn:de:0030-drops-174298}, doi = {10.4230/LIPIcs.FSTTCS.2022.37}, annote = {Keywords: Dominant Strategies, Compositional Synthesis, Reactive Synthesis} }

Document

**Published in:** LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

In the synthesis of distributed systems, we automate the development of distributed programs and hardware by automatically deriving correct implementations from formal specifications. For synchronous distributed systems, the synthesis problem is well known to be undecidable. For asynchronous systems, the boundary between decidable and undecidable synthesis problems is a long-standing open question. We study the problem in the setting of Petri games, a framework for distributed systems where asynchronous processes are equipped with causal memory. Petri games extend Petri nets with a distinction between system places and environment places. The components of a distributed system are the players of the game, represented as tokens that exchange information during each synchronization. Previous decidability results for this model are limited to local winning conditions, i.e., conditions that only refer to individual components.
In this paper, we consider global winning conditions such as mutual exclusion, i.e., conditions that refer to the state of all components. We provide decidability and undecidability results for global winning conditions. First, we prove for winning conditions given as bad markings that it is decidable whether a winning strategy for the system players exists in Petri games with a bounded number of system players and one environment player. Second, we prove for winning conditions that refer to both good and bad markings that it is undecidable whether a winning strategy for the system players exists in Petri games with at least two system players and one environment player. Our results thus show that, on the one hand, it is indeed possible to use global safety specifications like mutual exclusion in the synthesis of distributed systems. However, on the other hand, adding global liveness specifications results in an undecidable synthesis problem for almost all Petri games.

Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 20:1-20:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:LIPIcs.CSL.2022.20, author = {Finkbeiner, Bernd and Gieseking, Manuel and Hecking-Harbusch, Jesko and Olderog, Ernst-R\"{u}diger}, title = {{Global Winning Conditions in Synthesis of Distributed Systems with Causal Memory}}, booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)}, pages = {20:1--20:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-218-1}, ISSN = {1868-8969}, year = {2022}, volume = {216}, editor = {Manea, Florin and Simpson, Alex}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.20}, URN = {urn:nbn:de:0030-drops-157400}, doi = {10.4230/LIPIcs.CSL.2022.20}, annote = {Keywords: Synthesis, distributed systems, reactive systems, Petri games, decidability} }

Document

**Published in:** LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

We study the expressivity and complexity of model checking of linear temporal logic with team semantics (TeamLTL). TeamLTL, despite being a purely modal logic, is capable of defining hyperproperties, i.e., properties which relate multiple execution traces. TeamLTL has been introduced quite recently and only few results are known regarding its expressivity and its model checking problem. We relate the expressivity of TeamLTL to logics for hyperproperties obtained by extending LTL with trace and propositional quantifiers (HyperLTL and HyperQPTL). By doing so, we obtain a number of model checking results for TeamLTL and identify its undecidability frontier. In particular, we show decidability of model checking of the so-called left-flat fragment of any downward closed TeamLTL -extension. Moreover, we establish that the model checking problem of TeamLTL with Boolean disjunction and inclusion atoms is undecidable.

Jonni Virtema, Jana Hofmann, Bernd Finkbeiner, Juha Kontinen, and Fan Yang. Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 52:1-52:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{virtema_et_al:LIPIcs.FSTTCS.2021.52, author = {Virtema, Jonni and Hofmann, Jana and Finkbeiner, Bernd and Kontinen, Juha and Yang, Fan}, title = {{Linear-Time Temporal Logic with Team Semantics: Expressivity and Complexity}}, booktitle = {41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)}, pages = {52:1--52:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-215-0}, ISSN = {1868-8969}, year = {2021}, volume = {213}, editor = {Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.52}, URN = {urn:nbn:de:0030-drops-155634}, doi = {10.4230/LIPIcs.FSTTCS.2021.52}, annote = {Keywords: Linear temporal logic, Hyperproperties, Model Checking, Expressivity} }

Document

**Published in:** LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Hyperproperties are commonly used in computer security to define information-flow policies and other requirements that reason about the relationship between multiple computations. In this paper, we study a novel class of hyperproperties where the individual computation paths are chosen by the strategic choices of a coalition of agents in a multi-agent system. We introduce HyperATL^*, an extension of computation tree logic with path variables and strategy quantifiers. HyperATL^* can express strategic hyperproperties, such as that the scheduler in a concurrent system has a strategy to avoid information leakage. HyperATL^* is particularly useful to specify asynchronous hyperproperties, i.e., hyperproperties where the speed of the execution on the different computation paths depends on the choices of the scheduler. Unlike other recent logics for the specification of asynchronous hyperproperties, our logic is the first to admit decidable model checking for the full logic. We present a model checking algorithm for HyperATL^* based on alternating word automata, and show that our algorithm is asymptotically optimal by providing a matching lower bound. We have implemented a prototype model checker for a fragment of HyperATL^*, able to check various security properties on small programs.

Raven Beutner and Bernd Finkbeiner. A Temporal Logic for Strategic Hyperproperties. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 24:1-24:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{beutner_et_al:LIPIcs.CONCUR.2021.24, author = {Beutner, Raven and Finkbeiner, Bernd}, title = {{A Temporal Logic for Strategic Hyperproperties}}, booktitle = {32nd International Conference on Concurrency Theory (CONCUR 2021)}, pages = {24:1--24:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-203-7}, ISSN = {1868-8969}, year = {2021}, volume = {203}, editor = {Haddad, Serge and Varacca, Daniele}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.24}, URN = {urn:nbn:de:0030-drops-144019}, doi = {10.4230/LIPIcs.CONCUR.2021.24}, annote = {Keywords: hyperproperties, temporal logic, alternating-time temporal logic, model checking, multi-agent systems, information flow, asynchronous hyperproperties} }

Document

**Published in:** LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

In distributed synthesis, a set of process implementations is generated, which together, accomplish an objective against all possible behaviors of the environment. A lot of recent work has focussed on systems with causal memory, i.e., sets of asynchronous processes that exchange their causal histories upon synchronization. Decidability results for this problem have been stated either in terms of control games, which extend Zielonka’s asynchronous automata by partitioning the actions into controllable and uncontrollable, or in terms of Petri games, which extend Petri nets by partitioning the tokens into system and environment players. The precise connection between these two models was so far, however, an open question.
In this paper, we provide the first formal connection between control games and Petri games. We establish the equivalence of the two game types based on weak bisimulations between their strategies. For both directions, we show that a game of one type can be translated into an equivalent game of the other type. We provide exponential upper and lower bounds for the translations. Our translations allow to transfer and combine decidability results between the two types of games. Exemplarily, we translate decidability in acyclic communication architectures, originally obtained for control games, to Petri games, and decidability in single-process systems, originally obtained for Petri games, to control games.

Raven Beutner, Bernd Finkbeiner, and Jesko Hecking-Harbusch. Translating Asynchronous Games for Distributed Synthesis. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{beutner_et_al:LIPIcs.CONCUR.2019.26, author = {Beutner, Raven and Finkbeiner, Bernd and Hecking-Harbusch, Jesko}, title = {{Translating Asynchronous Games for Distributed Synthesis}}, booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)}, pages = {26:1--26:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-121-4}, ISSN = {1868-8969}, year = {2019}, volume = {140}, editor = {Fokkink, Wan and van Glabbeek, Rob}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.26}, URN = {urn:nbn:de:0030-drops-109289}, doi = {10.4230/LIPIcs.CONCUR.2019.26}, annote = {Keywords: synthesis, distributed systems, causal memory, Petri games, control games} }

Document

**Published in:** LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

We study the problem of determining whether a given temporal specification can be implemented by a symmetric system, i.e., a system composed from identical components. Symmetry is an important goal in the design of distributed systems, because systems that are composed from identical components are easier to build and maintain. We show that for the class of rotation-symmetric architectures, i.e., multi-process architectures where all processes have access to all system inputs, but see different rotations of the inputs, the symmetric synthesis problem is EXPTIME-complete in the number of processes. In architectures where the processes do not have access to all input variables, the symmetric synthesis problem becomes undecidable, even in cases where the standard distributed synthesis problem is decidable.

Rüdiger Ehlers and Bernd Finkbeiner. Symmetric Synthesis. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 26:1-26:13, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{ehlers_et_al:LIPIcs.FSTTCS.2017.26, author = {Ehlers, R\"{u}diger and Finkbeiner, Bernd}, title = {{Symmetric Synthesis}}, booktitle = {37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)}, pages = {26:1--26:13}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-055-2}, ISSN = {1868-8969}, year = {2018}, volume = {93}, editor = {Lokam, Satya and Ramanujam, R.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.26}, URN = {urn:nbn:de:0030-drops-83996}, doi = {10.4230/LIPIcs.FSTTCS.2017.26}, annote = {Keywords: Reactive Synthesis, Symmetry} }

Document

**Published in:** LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Most approaches to the synthesis of reactive systems study the problem in terms of a two-player game with complete observation. In many applications, however, the system's environment consists of several distinct entities, and the system must actively communicate with these entities in order to obtain information available in the environment. In this paper, we model such environments as a team of players and keep track of the information known to each individual player. This allows us to synthesize programs that interact with a distributed environment and leverage multiple interacting sources of information.
The synthesis problem in distributed environments corresponds to solving a special class of Petri games, i.e., multi-player games played over Petri nets, where the net has a distinguished token representing the system and an arbitrary number of tokens representing the environment. While, in general, even the decidability of Petri games is an open question, we show that the synthesis problem in distributed environments can be solved in polynomial time for nets with up to two environment tokens. For an arbitrary but fixed number of three or more environment tokens, the problem is NP-complete. If the number of environment tokens grows with the size of the net, the problem is EXPTIME-complete.

Bernd Finkbeiner and Paul Gölz. Synthesis in Distributed Environments. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 28:1-28:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:LIPIcs.FSTTCS.2017.28, author = {Finkbeiner, Bernd and G\"{o}lz, Paul}, title = {{Synthesis in Distributed Environments}}, booktitle = {37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)}, pages = {28:1--28:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-055-2}, ISSN = {1868-8969}, year = {2018}, volume = {93}, editor = {Lokam, Satya and Ramanujam, R.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.28}, URN = {urn:nbn:de:0030-drops-84068}, doi = {10.4230/LIPIcs.FSTTCS.2017.28}, annote = {Keywords: reactive synthesis, distributed information, causal memory, Petri nets} }

Document

**Published in:** LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)

We investigate the logical foundations of hyperproperties. Hyperproperties generalize trace properties, which are sets of traces, to sets of sets of traces. The most prominent application of hyperproperties is information flow security: information flow policies characterize the secrecy and integrity of a system by comparing two or more execution traces, for example by comparing the observations made by an external observer on execution traces that result from different values of a secret variable.
In this paper, we establish the first connection between temporal logics for hyperproperties and first-order logic. Kamp's seminal theorem (in the formulation due to Gabbay et al.) states that linear-time temporal logic (LTL) is expressively equivalent to first-order logic over the natural numbers with order. We introduce first-order logic over sets of traces and prove that HyperLTL, the extension of LTL to hyperproperties, is strictly subsumed by this logic. We furthermore exhibit a fragment that is expressively equivalent to HyperLTL, thereby establishing Kamp's theorem for hyperproperties.

Bernd Finkbeiner and Martin Zimmermann. The First-Order Logic of Hyperproperties. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 30:1-30:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:LIPIcs.STACS.2017.30, author = {Finkbeiner, Bernd and Zimmermann, Martin}, title = {{The First-Order Logic of Hyperproperties}}, booktitle = {34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)}, pages = {30:1--30:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-028-6}, ISSN = {1868-8969}, year = {2017}, volume = {66}, editor = {Vollmer, Heribert and Vall\'{e}e, Brigitte}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.30}, URN = {urn:nbn:de:0030-drops-70031}, doi = {10.4230/LIPIcs.STACS.2017.30}, annote = {Keywords: Hyperproperties, Linear Temporal Logic, First-order Logic} }

Document

**Published in:** LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Hyperproperties, like observational determinism or symmetry, cannot be expressed as properties of individual computation traces, because they describe a relation between multiple computation traces. HyperLTL is a temporal logic that captures such relations through trace variables, which are introduced through existential and universal trace quantifiers and can be used to refer to multiple computations at the same time. In this paper, we study the satisfiability problem of HyperLTL. We show that the problem is PSPACE-complete for alternation-free formulas (and, hence, no more expensive than LTL satisfiability), EXPSPACE-complete for exists-forall-formulas, and undecidable for forall-exists-formulas. Many practical hyperproperties can be expressed as alternation-free formulas. Our results show that both satisfiability and implication are decidable for such properties.

Bernd Finkbeiner and Christopher Hahn. Deciding Hyperproperties. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 13:1-13:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:LIPIcs.CONCUR.2016.13, author = {Finkbeiner, Bernd and Hahn, Christopher}, title = {{Deciding Hyperproperties}}, booktitle = {27th International Conference on Concurrency Theory (CONCUR 2016)}, pages = {13:1--13:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-017-0}, ISSN = {1868-8969}, year = {2016}, volume = {59}, editor = {Desharnais, Jos\'{e}e and Jagadeesan, Radha}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.13}, URN = {urn:nbn:de:0030-drops-61706}, doi = {10.4230/LIPIcs.CONCUR.2016.13}, annote = {Keywords: temporal logics, satisfiability, hyperproperties, complexity} }

Document

**Published in:** LIPIcs, Volume 2, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (2008)

Counterexample-guided abstraction refinement (CEGAR) is used in
automated software analysis to find suitable finite-state abstractions
of infinite-state systems. In this paper, we extend CEGAR to games
with incomplete information, as they commonly occur in controller
synthesis and modular verification. The challenge is that, under
incomplete information, one must carefully account for the knowledge
available to the player: the strategy must not depend on information
the player cannot see. We propose an abstraction mechanism for games under
incomplete information that incorporates the approximation of the players\' moves
into a knowledge-based subset construction on the abstract state
space. This abstraction results in a perfect-information game over a
finite graph. The concretizability of abstract strategies can be encoded as
the satisfiability of strategy-tree formulas. Based on this encoding,
we present an interpolation-based approach for selecting new predicates
and provide sufficient conditions for the termination of the resulting
refinement loop.

Rayna Dimitrova and Bernd Finkbeiner. Abstraction Refinement for Games with Incomplete Information. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 175-186, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{dimitrova_et_al:LIPIcs.FSTTCS.2008.1751, author = {Dimitrova, Rayna and Finkbeiner, Bernd}, title = {{Abstraction Refinement for Games with Incomplete Information}}, booktitle = {IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science}, pages = {175--186}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-08-8}, ISSN = {1868-8969}, year = {2008}, volume = {2}, editor = {Hariharan, Ramesh and Mukund, Madhavan and Vinay, V}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2008.1751}, URN = {urn:nbn:de:0030-drops-17510}, doi = {10.4230/LIPIcs.FSTTCS.2008.1751}, annote = {Keywords: Automatic abstraction refinement, synthesis} }

Document

**Published in:** Dagstuhl Seminar Proceedings, Volume 7011, Runtime Verification (2008)

From January 2--6 2007 the Dagstuhl Seminar 07011 {\em `Runtime Verification'}
was held in the International Conference and Research
Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented
their current research, and ongoing work and open problems were discussed.
Abstracts of the presentations given during the seminar have been put together in
this paper. The first section is an executive summary that describes the seminar topics
in general.

Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, and Oleg Sokolsky. 07011 Abstracts Collection – Runtime Verification. In Runtime Verification. Dagstuhl Seminar Proceedings, Volume 7011, pp. 1-15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:DagSemProc.07011.1, author = {Finkbeiner, Bernd and Havelund, Klaus and Rosu, Grigore and Sokolsky, Oleg}, title = {{07011 Abstracts Collection – Runtime Verification}}, booktitle = {Runtime Verification}, pages = {1--15}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2008}, volume = {7011}, editor = {Bernd Finkbeiner and Klaus Havelund and Grigore Rosu and Oleg Sokolsky}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07011.1}, URN = {urn:nbn:de:0030-drops-13764}, doi = {10.4230/DagSemProc.07011.1}, annote = {Keywords: Program monitoring, dynamic program analysis, specification languages and logics, concurrency errors, program instrumentation, aspect-oriented programming, test oracles, fault protection, dynamic specification learning, combining static and dynamic analysis} }

Document

**Published in:** Dagstuhl Seminar Proceedings, Volume 7011, Runtime Verification (2008)

From January 2 to January 6, 2007, the Dagstuhl Seminar
07011 "Runtime Verification" was held in the International Conference
and Research Center (IBFI), Schloss Dagstuhl. Over the past few years,
runtime verification has emerged as a focused subject in program analysis
that bridges the gap between the complexity-haunted field of fully formal
verification methods and the ad-hoc field of testing. Other terms for this
subject are: program monitoring, dynamic program analysis, and runtime
analysis. Thirty researchers participated in the seminar and discussed
their recent work and recent trends in runtime verification.

Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, and Oleg Sokolsky. 07011 Executive Summary – Runtime Verification. In Runtime Verification. Dagstuhl Seminar Proceedings, Volume 7011, pp. 1-3, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:DagSemProc.07011.2, author = {Finkbeiner, Bernd and Havelund, Klaus and Rosu, Grigore and Sokolsky, Oleg}, title = {{07011 Executive Summary – Runtime Verification}}, booktitle = {Runtime Verification}, pages = {1--3}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2008}, volume = {7011}, editor = {Bernd Finkbeiner and Klaus Havelund and Grigore Rosu and Oleg Sokolsky}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07011.2}, URN = {urn:nbn:de:0030-drops-13699}, doi = {10.4230/DagSemProc.07011.2}, annote = {Keywords: Program monitoring, dynamic program analysis, specification languages and logics, concurrency errors, program instrumentation, aspect-oriented program} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail