8 Search Results for "Wasowski, Andrzej"

Document
DOI: 10.4230/LIPIcs.CSL.2026.30
Reward Interfaces with Best-Effort Implementations

Authors: Rafael Dewes and Rayna Dimitrova

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Interface theories, notably interface automata, serve as expressive frameworks for component-based design, specifying component behavior and interaction in concurrent systems. Traditional interface formalisms specify assumptions that a component’s environment must satisfy and the guarantees that each component provides. This qualitative view of component interaction based on imposing strict assumptions and Boolean guarantees may, however, not be expressive enough to capture the system’s allowed or desired behaviors under different environments. In this paper, we introduce reward interfaces to support component-based design while accommodating multi-valued correctness requirements and adaptive best-effort satisfaction of component’s guarantees. Building upon interface automata, our framework enables modeling a rich class of quantitative component specifications. We propose formal notions of implementation, refinement and compatibility for reward interfaces. We study a class of reward interfaces with automata-based representations, for which we provide algorithms for checking compatibility and refinement, and existence of best-effort implementations. Our framework offers a comprehensive approach to reward interface specification and design.
Cite as

Rafael Dewes and Rayna Dimitrova. Reward Interfaces with Best-Effort Implementations. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 30:1-30:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{dewes_et_al:LIPIcs.CSL.2026.30,
  author =	{Dewes, Rafael and Dimitrova, Rayna},
  title =	{{Reward Interfaces with Best-Effort Implementations}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{30:1--30:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.30},
  URN =		{urn:nbn:de:0030-drops-254553},
  doi =		{10.4230/LIPIcs.CSL.2026.30},
  annote =	{Keywords: Component-based design, interface automata, quantitative specifications}
}
Artifact
Software
DOI: 10.4230/artifacts.24207
SAT-Metropolis

Authors: Maja Aaslyng Dall, Raúl Pardo, Thomas Lumley, and Andrzej Wąsowski

Abstract
Cite as

Maja Aaslyng Dall, Raúl Pardo, Thomas Lumley, Andrzej Wąsowski. SAT-Metropolis (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24207,
   title = {{SAT-Metropolis}}, 
   author = {Dall, Maja Aaslyng and Pardo, Ra\'{u}l and Lumley, Thomas and W\k{a}sowski, Andrzej},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:bfc2169353301af051d1af4488050fcfba06a849;origin=https://github.com/itu-square/sat-metropolis;visit=swh:1:snp:34a7c85d29d812f0a6738447fb21c25506f3bbb6;anchor=swh:1:rev:27112abeb8d3f532ef413da3437575d7170b2b84}{\texttt{swh:1:dir:bfc2169353301af051d1af4488050fcfba06a849}} (visited on 2025-08-07)},
   url = {https://github.com/itu-square/sat-metropolis},
   doi = {10.4230/artifacts.24207},
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.12
SAT-Metropolis: Combining Markov Chain Monte Carlo with SAT/SMT Sampling

Authors: Maja Aaslyng Dall, Raúl Pardo, Thomas Lumley, and Andrzej Wąsowski

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Probabilistic inference via Markov Chain Monte Carlo (MCMC) is at the core of statistical analysis and has a myriad of applications. However, probabilistic inference in the presence of hard constraints, so constraints that must hold with probability one, remains a difficult task. The reason is that hard constraints make the state space of the target distribution sparse, and may even divide it into disjoint areas separated by probability-zero states. As a consequence, the random walk performed by MCMC algorithms fails to effectively sample from the complete set of states in the target distribution. In this paper, we propose the use of SAT/SMT sampling to adapt a classic and widely used MCMC algorithm, namely Metropolis sampling. We use SAT/SMT samplers as proposal distributions. In this way, the algorithm ignores probability-zero states. Our method, sat-metropolis, effectively works in problems with multivariate polynomial hard constraints where regular Metropolis fails. We evaluate the convergence and scalability of sat-metropolis using three different state-of-the-art SAT/SMT samplers: SPUR, CMSGen, and MegaSampler. The evaluation shows how different features of the SAT/SMT sampling tools affect the effectiveness of probabilistic inference. We conclude that SAT/SMT sampling is a viable and promising technology for probabilistic inference under hard constraints.
Cite as

Maja Aaslyng Dall, Raúl Pardo, Thomas Lumley, and Andrzej Wąsowski. SAT-Metropolis: Combining Markov Chain Monte Carlo with SAT/SMT Sampling. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dall_et_al:LIPIcs.SAT.2025.12,
  author =	{Dall, Maja Aaslyng and Pardo, Ra\'{u}l and Lumley, Thomas and W\k{a}sowski, Andrzej},
  title =	{{SAT-Metropolis: Combining Markov Chain Monte Carlo with SAT/SMT Sampling}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{12:1--12:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.12},
  URN =		{urn:nbn:de:0030-drops-237462},
  doi =		{10.4230/LIPIcs.SAT.2025.12},
  annote =	{Keywords: SAT/SMT sampling, Probabilistic inference, Markov Chain Monte Carlo}
}
Document
DOI: 10.4230/LITES.8.2.4
A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems

Authors: Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
Designing and modeling complex cyber-physical systems (CPS) faces the double challenge of combined discrete-continuous dynamics and concurrent behavior. Existing formal modeling and verification languages for CPS expose the underlying proof search technology. They lack high-level structuring elements and are not efficiently executable. The ensuing modeling gap renders formal CPS models hard to understand and to validate. We propose a high-level programming-based approach to formal modeling and verification of hybrid systems as a hybrid extension of an Active Objects language. Well-structured hybrid active programs and requirements allow automatic, reachability-preserving translation into differential dynamic logic, a logic for hybrid (discrete-continuous) programs. Verification is achieved by discharging the resulting formulas with the theorem prover KeYmaera X. We demonstrate the usability of our approach with case studies.
Cite as

Eduard Kamburjan, Stefan Mitsch, and Reiner Hähnle. A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 04:1-04:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{kamburjan_et_al:LITES.8.2.4,
  author =	{Kamburjan, Eduard and Mitsch, Stefan and H\"{a}hnle, Reiner},
  title =	{{A Hybrid Programming Language for Formal Modeling and Verification of Hybrid Systems}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{04:1--04:34},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.4},
  URN =		{urn:nbn:de:0030-drops-192965},
  doi =		{10.4230/LITES.8.2.4},
  annote =	{Keywords: Active Objects, Differential Dynamic Logic, Hybrid Systems}
}
Document
DOI: 10.4230/LITES.8.2.3
Higher-Dimensional Timed and Hybrid Automata

Authors: Uli Fahrenberg

Published in: LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2

Abstract
We introduce a new formalism of higher-dimensional timed automata, based on Pratt and van Glabbeek’s higher-dimensional automata and Alur and Dill’s timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also extend the setting to higher-dimensional hybrid automata.The interest of our formalism is in modeling systems which exhibit both real-time behavior and concurrency. Other existing formalisms for real-time modeling identify concurrency and interleaving, which, as we shall argue, is problematic.
Cite as

Uli Fahrenberg. Higher-Dimensional Timed and Hybrid Automata. In LITES, Volume 8, Issue 2 (2022): Special Issue on Distributed Hybrid Systems. Leibniz Transactions on Embedded Systems, Volume 8, Issue 2, pp. 03:1-03:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{fahrenberg:LITES.8.2.3,
  author =	{Fahrenberg, Uli},
  title =	{{Higher-Dimensional Timed and Hybrid Automata}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{03:1--03:16},
  ISSN =	{2199-2002},
  year =	{2022},
  volume =	{8},
  number =	{2},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LITES.8.2.3},
  URN =		{urn:nbn:de:0030-drops-192951},
  doi =		{10.4230/LITES.8.2.3},
  annote =	{Keywords: timed automaton, higher-dimensional automaton, precubical set, real time, non-interleaving concurrency, hybrid automaton}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2015.247
Variability Abstractions: Trading Precision for Speed in Family-Based Analyses

Authors: Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)

Abstract
Family-based (lifted) data-flow analysis for Software Product Lines (SPLs) is capable of analyzing all valid products (variants) without generating any of them explicitly. It takes as input only the common code base, which encodes all variants of a SPL, and produces analysis results corresponding to all variants. However, the computational cost of the lifted analysis still depends inherently on the number of variants (which is exponential in the number of features, in the worst case). For a large number of features, the lifted analysis may be too costly or even infeasible. In this paper, we introduce variability abstractions defined as Galois connections and use abstract interpretation as a formal method for the calculational-based derivation of approximate (abstracted) lifted analyses of SPL programs, which are sound by construction. Moreover, given an abstraction we define a syntactic transformation that translates any SPL program into an abstracted version of it, such that the analysis of the abstracted SPL coincides with the corresponding abstracted analysis of the original SPL. We implement the transformation in a tool, that works on Object-Oriented Java program families, and evaluate the practicality of this approach on three Java SPL benchmarks.
Cite as

Aleksandar S. Dimovski, Claus Brabrand, and Andrzej Wasowski. Variability Abstractions: Trading Precision for Speed in Family-Based Analyses. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 247-270, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{dimovski_et_al:LIPIcs.ECOOP.2015.247,
  author =	{Dimovski, Aleksandar S. and Brabrand, Claus and Wasowski, Andrzej},
  title =	{{Variability Abstractions: Trading Precision for Speed in Family-Based Analyses}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{247--270},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.247},
  URN =		{urn:nbn:de:0030-drops-52253},
  doi =		{10.4230/LIPIcs.ECOOP.2015.247},
  annote =	{Keywords: Software Product Lines, Family-Based Program Analysis, Abstract Interpretation}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.517
Information Leakage of Non-Terminating Processes

Authors: Fabrizio Biondi, Axel Legay, Bo Friis Nielsen, Pasquale Malacaria, and Andrzej Wasowski

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
In recent years, quantitative security techniques have been providing effective measures of the security of a system against an attacker. Such techniques usually assume that the system produces a finite amount of observations based on a finite amount of secret bits and terminates, and the attack is based on these observations. By modeling systems with Markov chains, we are able to measure the effectiveness of attacks on non-terminating systems. Such systems do not necessarily produce a finite amount of output and are not necessarily based on a finite amount of secret bits. We provide characterizations and algorithms to define meaningful measures of security for non-terminating systems, and to compute them when possible. We also study the bounded versions of the problems, and show examples of non-terminating programs and how their effectiveness in protecting their secret can be measured.
Cite as

Fabrizio Biondi, Axel Legay, Bo Friis Nielsen, Pasquale Malacaria, and Andrzej Wasowski. Information Leakage of Non-Terminating Processes. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 517-529, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{biondi_et_al:LIPIcs.FSTTCS.2014.517,
  author =	{Biondi, Fabrizio and Legay, Axel and Nielsen, Bo Friis and Malacaria, Pasquale and Wasowski, Andrzej},
  title =	{{Information Leakage of Non-Terminating Processes}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{517--529},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.517},
  URN =		{urn:nbn:de:0030-drops-48683},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.517},
  annote =	{Keywords: Quantitative information flow, Markov chain, information leakage, infinite execution}
}
Document
DOI: 10.4230/DagRep.3.2.144
Analysis, Test and Verification in The Presence of Variability (Dagstuhl Seminar 13091)

Authors: Paulo Borba, Myra B. Cohen, Axel Legay, and Andrzej Wasowski

Published in: Dagstuhl Reports, Volume 3, Issue 2 (2013)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 13091 "Analysis, Test and Verification in The Presence of Variability". The seminar had the goal of consolidating and stimulating research on analysis of software models with variability, enabling the design of variability-aware tool chains. We brought together 46 key researchers from three continents, working on quality assurance challenges that arise from introducing variability, and some who do not work with variability, but that are experts in their respective areas in the broader domain of software analysis or testing research. As a result of interactions triggered by sessions of different formats, the participants were able to classify their approaches with respect to a number of dimensions that helped to identify similarities and differences that have already been useful to improve understanding and foster new collaborations among the participants.
Cite as

Paulo Borba, Myra B. Cohen, Axel Legay, and Andrzej Wasowski. Analysis, Test and Verification in The Presence of Variability (Dagstuhl Seminar 13091). In Dagstuhl Reports, Volume 3, Issue 2, pp. 144-170, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{borba_et_al:DagRep.3.2.144,
  author =	{Borba, Paulo and Cohen, Myra B. and Legay, Axel and Wasowski, Andrzej},
  title =	{{Analysis, Test and Verification in The Presence of Variability (Dagstuhl Seminar 13091)}},
  pages =	{144--170},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{3},
  number =	{2},
  editor =	{Borba, Paulo and Cohen, Myra B. and Legay, Axel and Wasowski, Andrzej},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.3.2.144},
  URN =		{urn:nbn:de:0030-drops-40207},
  doi =		{10.4230/DagRep.3.2.144},
  annote =	{Keywords: Verification, Program Analysis, Testing, Semantics of Programming Languages, Software Engineering}
}
  • Refine by Type
  • 7 Document/PDF
  • 2 Document/HTML
  • 1 Artifact

  • Refine by Publication Year
  • 1 2026
  • 2 2025
  • 2 2022
  • 1 2015
  • 1 2014
  • Show More...

  • Refine by Author
  • 3 Wasowski, Andrzej
  • 2 Dall, Maja Aaslyng
  • 2 Legay, Axel
  • 2 Lumley, Thomas
  • 2 Pardo, Raúl
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs
  • 2 LITES
  • 1 DagRep

  • Refine by Classification
  • 2 Theory of computation → Timed and hybrid models
  • 1 Computing methodologies → Distributed programming languages
  • 1 Computing methodologies → Model verification and validation
  • 1 Mathematics of computing
  • 1 Theory of computation → Concurrency
  • Show More...

  • Refine by Keyword
  • 1 Abstract Interpretation
  • 1 Active Objects
  • 1 Component-based design
  • 1 Differential Dynamic Logic
  • 1 Family-Based Program Analysis
  • 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