18 Search Results for "Havelund, Klaus"

Document
Short Paper
DOI: 10.4230/OASIcs.DX.2025.13
Beyond Dynamic Bayesian Networks: Fusing Temporal Logic Monitors with Probabilistic Diagnosis (Short Paper)

Authors: Chetan Kulkarni and Johann Schumann

Published in: OASIcs, Volume 136, 36th International Conference on Principles of Diagnosis and Resilient Systems (DX 2025)

Abstract
Conventional diagnostic systems often fail to account for temporal dynamics - such as duration, frequency, or sequence of events - which are critical for accurate fault assessment. Existing solutions that model time, like Dynamic Bayesian Networks (DBNs), typically suffer from computational complexity and scalability issues. This paper introduces a hybrid diagnostic architecture that integrates a standard Bayesian Networks (BNs) with a powerful temporal reasoner R2U2 (Realizable Responsive Unobtrusive Unit). By decoupling temporal logic from probabilistic inference, our approach allows the specialized R2U2 engine to efficiently process complex time-dependent conditions and provide nuanced inputs to the BNs. The result is a more scalable, flexible, and robust framework for diagnosing failures in systems where temporal behavior is a key factor. The paper will detail this architecture, its generation from system models, and demonstrate its capabilities using a UAV electric powertrain example.
Cite as

Chetan Kulkarni and Johann Schumann. Beyond Dynamic Bayesian Networks: Fusing Temporal Logic Monitors with Probabilistic Diagnosis (Short Paper). In 36th International Conference on Principles of Diagnosis and Resilient Systems (DX 2025). Open Access Series in Informatics (OASIcs), Volume 136, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{kulkarni_et_al:OASIcs.DX.2025.13,
  author =	{Kulkarni, Chetan and Schumann, Johann},
  title =	{{Beyond Dynamic Bayesian Networks: Fusing Temporal Logic Monitors with Probabilistic Diagnosis}},
  booktitle =	{36th International Conference on Principles of Diagnosis and Resilient Systems (DX 2025)},
  pages =	{13:1--13:17},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-394-2},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{136},
  editor =	{Quinones-Grueiro, Marcos and Biswas, Gautam and Pill, Ingo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.DX.2025.13},
  URN =		{urn:nbn:de:0030-drops-248022},
  doi =		{10.4230/OASIcs.DX.2025.13},
  annote =	{Keywords: Bayesian diagnostic network, temporal logic, fault diagnosis, temporal reasoning, probabilistic inference, scalability}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.5
A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching

Authors: Joshua M. Cohen

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Algebraic data types (ADTs) and pattern matching are widely used to write elegant functional programs and to specify program behavior. These constructs are critical to most general-purpose interactive theorem provers (e.g. Lean, Rocq/Coq), first-order SMT-based deductive verifiers (e.g. Dafny, VeriFast), and intermediate verification languages (e.g. Why3). Such features require layers of compilation - in Rocq, pattern matches are compiled to remove nesting, while SMT-based tools further axiomatize ADTs with a first-order specification. However, these critical steps have been omitted from prior formalizations of such toolchains (e.g. MetaRocq). We give the first proved-sound sophisticated pattern matching compiler (based on Maranget’s compilation to decision trees) and first-order axiomatization of ADTs, both based on Why3 implementations. We prove the soundness of exhaustiveness checking, extending pen-and-paper proofs from the literature, and formulate a robustness property with which we find an exhaustiveness-related bug in Why3. We show that many of our proofs could be useful for reasoning about any first-order program verifier supporting ADTs.
Cite as

Joshua M. Cohen. A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cohen:LIPIcs.ITP.2025.5,
  author =	{Cohen, Joshua M.},
  title =	{{A Mechanized First-Order Theory of Algebraic Data Types with Pattern Matching}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{5:1--5:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.5},
  URN =		{urn:nbn:de:0030-drops-246046},
  doi =		{10.4230/LIPIcs.ITP.2025.5},
  annote =	{Keywords: Pattern Matching Compilation, Algebraic Data Types, First-Order Logic}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.19
Time for Timed Monitorability

Authors: Thomas M. Grosen, Sean Kauffman, Kim G. Larsen, and Martin Zimmermann

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Monitoring is an important part of the verification toolbox, in particular in situations where exhaustive verification using, e.g., model-checking is infeasible. The goal of online monitoring is to determine the satisfaction or violation of a specification during runtime, i.e., based on finite execution prefixes. However, not every specification is amenable to monitoring, e.g., properties for which no finite execution can witness satisfaction or violation. Monitorability is the question of whether a given specification is amenable to monitoring, and has been extensively studied in discrete time. Here, we study the monitorability problem for real-time properties expressed as Timed Automata. For specifications given by deterministic Timed Muller Automata, we prove decidability while we show that the problem is undecidable for specifications given by nondeterministic Timed Büchi automata. Furthermore, we refine monitorability to also determine bounds on the number of events as well as the time that must pass before monitoring the property may yield an informative verdict. We prove that for deterministic Timed Muller automata, such bounds can be effectively computed. In contrast we show that for nondeterministic Timed Büchi automata such bounds are not computable.
Cite as

Thomas M. Grosen, Sean Kauffman, Kim G. Larsen, and Martin Zimmermann. Time for Timed Monitorability. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{grosen_et_al:LIPIcs.CONCUR.2025.19,
  author =	{Grosen, Thomas M. and Kauffman, Sean and Larsen, Kim G. and Zimmermann, Martin},
  title =	{{Time for Timed Monitorability}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{19:1--19:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.19},
  URN =		{urn:nbn:de:0030-drops-239690},
  doi =		{10.4230/LIPIcs.CONCUR.2025.19},
  annote =	{Keywords: Monitorability, Monitoring, Timed Automata, MITL}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.26
Optimal Concolic Dynamic Partial Order Reduction

Authors: Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar, and Srinidhi Nagendra

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Stateless model checking (SMC) software implementations requires exploring both concurrency- and data nondeterminism. Unfortunately, most SMC algorithms focus on efficient exploration of concurrency nondeterminism, thereby neglecting an important source of bugs. We present ConDpor, an SMC algorithm for unmodified Java programs that combines optimal dynamic partial order reduction (DPOR) for concurrency nondeterminism, with concolic execution for data nondeterminism. ConDpor is sound, complete, optimal, and parametric w.r.t. the memory consistency model. Our experiments confirm that ConDpor is exponentially faster than DPOR with small-domain enumeration. Overall, ConDpor opens the door for efficient exploration of concurrent programs with data nondeterminism.
Cite as

Mohammad Hossein Khoshechin Jorshari, Michalis Kokologiannakis, Rupak Majumdar, and Srinidhi Nagendra. Optimal Concolic Dynamic Partial Order Reduction. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{khoshechinjorshari_et_al:LIPIcs.CONCUR.2025.26,
  author =	{Khoshechin Jorshari, Mohammad Hossein and Kokologiannakis, Michalis and Majumdar, Rupak and Nagendra, Srinidhi},
  title =	{{Optimal Concolic Dynamic Partial Order Reduction}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{26:1--26:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.26},
  URN =		{urn:nbn:de:0030-drops-239765},
  doi =		{10.4230/LIPIcs.CONCUR.2025.26},
  annote =	{Keywords: Stateless model checking, dynamic symbolic execution}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.22
Partial-Order Reduction Is Hard

Authors: Frédéric Herbreteau, Sarah Larroze-Jardiné, and Igor Walukiewicz

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
The goal of partial-order methods is to accelerate the exploration of concurrent systems by examining only a representative subset of all possible runs. The stateful approach builds a transition system with representative runs, while the stateless method simply enumerates them. The stateless approach may be preferable if the transition system is tree-like; otherwise, the stateful method is more effective. In the last decade, optimality has been a guiding principle for developing stateless partial-order reduction algorithms, and without doubt contributed to big progress in the field. In this paper we ask if we can get a similar principle for the stateful approach. We show that in stateful exploration, a polynomially close to optimal partial-order algorithm cannot exist unless P=NP. The result holds even for acyclic programs with just await instructions. This lower bound result justifies systematic study of heuristics for stateful partial-order reduction. We propose a notion of IFS oracle as a useful abstraction. The oracle can be used to get a very simple optimal stateless algorithm, which can then be adapted to a non-optimal stateful algorithm. While in general the oracle problem is NP-hard, we show a simple case where it can be solved in linear time.
Cite as

Frédéric Herbreteau, Sarah Larroze-Jardiné, and Igor Walukiewicz. Partial-Order Reduction Is Hard. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{herbreteau_et_al:LIPIcs.CONCUR.2025.22,
  author =	{Herbreteau, Fr\'{e}d\'{e}ric and Larroze-Jardin\'{e}, Sarah and Walukiewicz, Igor},
  title =	{{Partial-Order Reduction Is Hard}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{22:1--22:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.22},
  URN =		{urn:nbn:de:0030-drops-239727},
  doi =		{10.4230/LIPIcs.CONCUR.2025.22},
  annote =	{Keywords: Formal verification, Concurrent systems, Partial-order reduction, Complexity}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2025.4
Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory

Authors: Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
Runtime verification consists in checking whether a system satisfies a given specification by observing the execution trace it produces. In the regular setting, the modal μ-calculus provides a versatile formalism for expressing specifications of the control flow of the system. This paper focuses on the data flow and studies an extension of that logic that allows it to express data-dependent properties, identifying fragments that can be verified at runtime and with what correctness guarantees. The logic studied here is closely related with register automata with guessing. That correspondence yields a monitor synthesis algorithm, and a strict hierarchy among the various fragments of the logic, in contrast to the regular setting. We then exhibit a fragment of the logic that can express all monitorable formulae in the logic without greatest fixed-points but not in the full logic, and show this is the best we can get.
Cite as

Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Léo Exibard, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen. Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2025.4,
  author =	{Aceto, Luca and Achilleos, Antonis and Attard, Duncan Paul and Exibard, L\'{e}o and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna and Lehtinen, Karoliina},
  title =	{{Monitorability for the Modal Mu-Calculus over Systems with Data: From Practice to Theory}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.4},
  URN =		{urn:nbn:de:0030-drops-239546},
  doi =		{10.4230/LIPIcs.CONCUR.2025.4},
  annote =	{Keywords: Runtime verification, monitorability, \muHML with data, register automata}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.28
Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis

Authors: Mamy Razafintsialonina, David Bühler, Antoine Miné, Valentin Perrelle, and Julien Signoles

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Static analysis by means of abstract interpretation is a tool of choice for proving absence of some classes of errors, typically undefined behaviors in C code, in a sound way. However, static analysis tools are hardly integrated in CI/CD processes. One of the main reasons is that they are still time- and memory-expensive to apply after every single patch when developing a program. For solving this issue, incremental static analysis helps developers quickly obtain analysis results after making changes to a program. However, existing approaches are often not guaranteed to be sound, limited to specific analyses, or tied to specific tools. This limits their generalizability and applicability in practice, especially for large and critical software. In this paper, we propose a generic, sound approach to incremental static analysis that is applicable to any abstract interpreter. Our approach leverages the similarity between two versions of a program to soundly reuse previously computed analysis results. We introduce novel methods for summarizing functions and reusing loop invariants. They significantly reduce the cost of reanalysis, while maintaining soundness and a high level of precision. We have formalized our approach, proved it sound, implemented it in Eva, the abstract interpreter of Frama-C, and evaluated it on a set of real-world commits of open-source programs.
Cite as

Mamy Razafintsialonina, David Bühler, Antoine Miné, Valentin Perrelle, and Julien Signoles. Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 28:1-28:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{razafintsialonina_et_al:LIPIcs.ECOOP.2025.28,
  author =	{Razafintsialonina, Mamy and B\"{u}hler, David and Min\'{e}, Antoine and Perrelle, Valentin and Signoles, Julien},
  title =	{{Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{28:1--28:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.28},
  URN =		{urn:nbn:de:0030-drops-233207},
  doi =		{10.4230/LIPIcs.ECOOP.2025.28},
  annote =	{Keywords: Abstract Interpretation, Static Analysis, Incremental Analysis}
}
Document
Pearl/Brave New Idea
DOI: 10.4230/LIPIcs.ECOOP.2025.42
Contract Systems Need Domain-Specific Notations (Pearl/Brave New Idea)

Authors: Cameron Moy, Ryan Jung, and Matthias Felleisen

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Contract systems enable programmers to state specifications and have them enforced at run time. First-order contracts are expressed using ordinary code, while higher-order contracts are expressed using the notation familiar from type systems. Most interface descriptions, though, come with properties that involve not just assertions about single method calls, but entire call chains. Typical contract systems cannot express these specifications concisely. Such specifications demand domain-specific notations. In response, this paper proposes that contract systems abstract over the notation used for stating specifications. It presents an architecture for such a system, some illustrative examples, and an evaluation in terms of common notations from the literature.
Cite as

Cameron Moy, Ryan Jung, and Matthias Felleisen. Contract Systems Need Domain-Specific Notations (Pearl/Brave New Idea). In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 42:1-42:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{moy_et_al:LIPIcs.ECOOP.2025.42,
  author =	{Moy, Cameron and Jung, Ryan and Felleisen, Matthias},
  title =	{{Contract Systems Need Domain-Specific Notations}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{42:1--42:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.42},
  URN =		{urn:nbn:de:0030-drops-233348},
  doi =		{10.4230/LIPIcs.ECOOP.2025.42},
  annote =	{Keywords: software contracts, domain-specific languages}
}
Document
DOI: 10.4230/LIPIcs.STACS.2025.19
The Complexity of Learning LTL, CTL and ATL Formulas

Authors: Benjamin Bordais, Daniel Neider, and Rajarshi Roy

Published in: LIPIcs, Volume 327, 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)

Abstract
We consider the problem of learning temporal logic formulas from examples of system behavior. Learning temporal properties has crystallized as an effective means to explain complex temporal behaviors. Several efficient algorithms have been designed for learning temporal formulas. However, the theoretical understanding of the complexity of the learning decision problems remains largely unexplored. To address this, we study the complexity of the passive learning problems of three prominent temporal logics, Linear Temporal Logic (LTL), Computation Tree Logic (CTL) and Alternating-time Temporal Logic (ATL) and several of their fragments. We show that learning formulas with unbounded occurrences of binary operators is NP-complete for all of these logics. On the other hand, when investigating the complexity of learning formulas with bounded occurrences of binary operators, we exhibit discrepancies between the complexity of learning LTL, CTL and ATL formulas (with a varying number of agents).
Cite as

Benjamin Bordais, Daniel Neider, and Rajarshi Roy. The Complexity of Learning LTL, CTL and ATL Formulas. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 19:1-19:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bordais_et_al:LIPIcs.STACS.2025.19,
  author =	{Bordais, Benjamin and Neider, Daniel and Roy, Rajarshi},
  title =	{{The Complexity of Learning LTL, CTL and ATL Formulas}},
  booktitle =	{42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025)},
  pages =	{19:1--19:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-365-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{327},
  editor =	{Beyersdorff, Olaf and Pilipczuk, Micha{\l} and Pimentel, Elaine and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2025.19},
  URN =		{urn:nbn:de:0030-drops-228441},
  doi =		{10.4230/LIPIcs.STACS.2025.19},
  annote =	{Keywords: Temporal logic, passive learning, complexity}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.1
Locally Static, Globally Dynamic Session Types for Active Objects

Authors: Reiner Hähnle, Anton W. Haubner, and Eduard Kamburjan

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
Active object languages offer an attractive trade-off between low-level, preemptive concurrency and fully distributed actors: syntactically identifiable atomic code segments and asynchronous calls are the basis of cooperative concurrency, still permitting interleaving, but nevertheless being mechanically analyzable. The challenge is to reconcile local static analysis of atomic segments with the global scheduling constraints it depends on. Here, we propose an approximate, hybrid approach; At compile-time we perform a local static analysis: later, any run not complying to a global specification is excluded via runtime checks. That specification is expressed in a type-theoretic language inspired by session types. The approach reverses the usual (first global, then local) order of analysis and, thereby, supports analysis of open distributed systems.
Cite as

Reiner Hähnle, Anton W. Haubner, and Eduard Kamburjan. Locally Static, Globally Dynamic Session Types for Active Objects. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 1:1-1:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{hahnle_et_al:OASIcs.Gabbrielli.1,
  author =	{H\"{a}hnle, Reiner and Haubner, Anton W. and Kamburjan, Eduard},
  title =	{{Locally Static, Globally Dynamic Session Types for Active Objects}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{1:1--1:24},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.1},
  URN =		{urn:nbn:de:0030-drops-132237},
  doi =		{10.4230/OASIcs.Gabbrielli.1},
  annote =	{Keywords: Session Types, Active Objects, Runtime Verification, Static Verification}
}
Document
DOI: 10.4230/OASIcs.Gabbrielli.10
Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages

Authors: Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa, and Lars Tveito

Published in: OASIcs, Volume 86, Recent Developments in the Design and Implementation of Programming Languages (2020)

Abstract
This paper presents a method for testing whether objects in actor languages and active object languages exhibit locally deterministic behavior. We investigate such a method for a class of guarded command programs, abstracting from object-oriented features like method calls but focusing on cooperative scheduling of dynamically spawned processes executing in parallel. The proposed method can answer questions such as whether all permutations of an execution trace are equivalent, by generating candidate traces for testing which may lead to different final states. To prune the set of candidate traces, we employ partial order reduction. To further reduce the set, we introduce an analysis technique to decide whether a generated trace is schedulable. Schedulability cannot be decided for guarded commands using standard dependence and interference relations because guard enabledness is non-monotonic. To solve this problem, we use concolic execution to produce linearized symbolic traces of the executed program, which allows a weakest precondition computation to decide on the satisfiability of guards.
Cite as

Frank S. de Boer, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa, and Lars Tveito. Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages. In Recent Developments in the Design and Implementation of Programming Languages. Open Access Series in Informatics (OASIcs), Volume 86, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{deboer_et_al:OASIcs.Gabbrielli.10,
  author =	{de Boer, Frank S. and Johnsen, Einar Broch and Schlatte, Rudolf and Tapia Tarifa, Silvia Lizeth and Tveito, Lars},
  title =	{{Inseguendo Fagiani Selvatici: Partial Order Reduction for Guarded Command Languages}},
  booktitle =	{Recent Developments in the Design and Implementation of Programming Languages},
  pages =	{10:1--10:18},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-171-9},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{86},
  editor =	{de Boer, Frank S. and Mauro, Jacopo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.Gabbrielli.10},
  URN =		{urn:nbn:de:0030-drops-132322},
  doi =		{10.4230/OASIcs.Gabbrielli.10},
  annote =	{Keywords: Testing, Symbolic Traces, Guarded Commands, Partial Order Reduction}
}
Document
DOI: 10.4230/DagRep.7.11.59
A Shared Challenge in Behavioural Specification (Dagstuhl Seminar 17462)

Authors: Klaus Havelund, Martin Leucker, Giles Reger, and Volker Stolz

Published in: Dagstuhl Reports, Volume 7, Issue 11 (2018)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 17462 "A Shared Challenge in Behavioural Specification". The seminar considered the issue of behavioral specification with a focus on its usage in Runtime Verification. The seminar was motivated by the observations that, whilst the field of Runtime Verification is becoming more mature, there is a lack of common specification language, in the main part due to the rich setting allowing for highly expressive languages. The aim of the Seminar was to shed light on the similarities and differences between the different existing languages, and specifically, suggest directions for future collaboration and research. The seminar consisted of two talk sessions, two working group sessions, and a feedback and reflection session. Working group topics were suggested and agreed in response to points raised in talks. One significant outcome was the proposal of a shared challenge project in which different Runtime Verification approaches can be compared, as outlined in one of the working group reports.
Cite as

Klaus Havelund, Martin Leucker, Giles Reger, and Volker Stolz. A Shared Challenge in Behavioural Specification (Dagstuhl Seminar 17462). In Dagstuhl Reports, Volume 7, Issue 11, pp. 59-85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{havelund_et_al:DagRep.7.11.59,
  author =	{Havelund, Klaus and Leucker, Martin and Reger, Giles and Stolz, Volker},
  title =	{{A Shared Challenge in Behavioural Specification (Dagstuhl Seminar 17462)}},
  pages =	{59--85},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{7},
  number =	{11},
  editor =	{Havelund, Klaus and Leucker, Martin and Reger, Giles and Stolz, Volker},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.7.11.59},
  URN =		{urn:nbn:de:0030-drops-86716},
  doi =		{10.4230/DagRep.7.11.59},
  annote =	{Keywords: behavioural specification, dynamic properties, runtime verification, temporal logic}
}
Document
DOI: 10.4230/DagSemProc.10451.1
10451 Abstracts Collection – Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems

Authors: Klaus Havelund, Martin Leucker, Martin Sachenbacher, Oleg Sokolsky, and Brian C. Williams

Published in: Dagstuhl Seminar Proceedings, Volume 10451, Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems (2011)

Abstract
From November 7 to 12, 2010, the Dagstuhl Seminar 10451 ``Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems'' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, 35 participants presented their current research and discussed ongoing work and open problems. This document puts together abstracts of the presentations given during the seminar, and provides links to extended abstracts or full papers, if available.
Cite as

Klaus Havelund, Martin Leucker, Martin Sachenbacher, Oleg Sokolsky, and Brian C. Williams. 10451 Abstracts Collection – Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems. In Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems. Dagstuhl Seminar Proceedings, Volume 10451, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{havelund_et_al:DagSemProc.10451.1,
  author =	{Havelund, Klaus and Leucker, Martin and Sachenbacher, Martin and Sokolsky, Oleg and Williams, Brian C.},
  title =	{{10451 Abstracts Collection – Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems}},
  booktitle =	{Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2011},
  volume =	{10451},
  editor =	{Klaus Havelund and Martin Leucker and Martin Sachenbacher and Oleg Sokolsky and Brian C. Williams},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10451.1},
  URN =		{urn:nbn:de:0030-drops-29487},
  doi =		{10.4230/DagSemProc.10451.1},
  annote =	{Keywords: Runtime Verification, Model-based Diagnosis, Planning, Control, Autonomous Systems}
}
Document
DOI: 10.4230/DagSemProc.10451.2
10451 Executive Summary – Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems

Authors: Klaus Havelund, Martin Leucker, Martin Sachenbacher, Oleg Sokolsky, and Brian C. Williams

Published in: Dagstuhl Seminar Proceedings, Volume 10451, Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems (2011)

Abstract
From November 7 to 12, 2010, the Dagstuhl Seminar 10451 'Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems' was held in Schloss Dagstuhl – Leibniz Center for Informatics. During the seminar, 35 participants presented their current research and discussed ongoing work and open problems. This document puts together abstracts of the presentations given during the seminar, and provides links to extended abstracts or full papers, if available.
Cite as

Klaus Havelund, Martin Leucker, Martin Sachenbacher, Oleg Sokolsky, and Brian C. Williams. 10451 Executive Summary – Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems. In Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems. Dagstuhl Seminar Proceedings, Volume 10451, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{havelund_et_al:DagSemProc.10451.2,
  author =	{Havelund, Klaus and Leucker, Martin and Sachenbacher, Martin and Sokolsky, Oleg and Williams, Brian C.},
  title =	{{10451 Executive Summary – Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems}},
  booktitle =	{Runtime Verification, Diagnosis, Planning and Control for Autonomous Systems},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2011},
  volume =	{10451},
  editor =	{Klaus Havelund and Martin Leucker and Martin Sachenbacher and Oleg Sokolsky and Brian C. Williams},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.10451.2},
  URN =		{urn:nbn:de:0030-drops-29476},
  doi =		{10.4230/DagSemProc.10451.2},
  annote =	{Keywords: Runtime Verification, Model-based Diagnosis, Planning, Control, Autonomous Systems}
}
Document
DOI: 10.4230/DagSemProc.07011.2
07011 Executive Summary – Runtime Verification

Authors: Bernd Finkbeiner, Klaus Havelund, Grigore Rosu, and Oleg Sokolsky

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

Abstract
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.
Cite as

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}
}
  • Refine by Type
  • 18 Document/PDF
  • 9 Document/HTML

  • Refine by Publication Year
  • 9 2025
  • 2 2020
  • 1 2018
  • 2 2011
  • 4 2008

  • Refine by Author
  • 5 Havelund, Klaus
  • 5 Sokolsky, Oleg
  • 3 Leucker, Martin
  • 2 Finkbeiner, Bernd
  • 2 Rosu, Grigore
  • Show More...

  • Refine by Series/Journal
  • 8 LIPIcs
  • 3 OASIcs
  • 1 DagRep
  • 6 DagSemProc

  • Refine by Classification
  • 4 Theory of computation → Logic and verification
  • 2 Software and its engineering → Semantics
  • 2 Theory of computation → Modal and temporal logics
  • 1 Computing methodologies → Causal reasoning and diagnostics
  • 1 Computing methodologies → Multiscale systems
  • Show More...

  • Refine by Keyword
  • 3 Runtime Verification
  • 2 Autonomous Systems
  • 2 Control
  • 2 Model-based Diagnosis
  • 2 Monitoring
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact