Algorithms and Logics for Verification

Research output

Content available in repository 2012 2023 2024 2025

• 58 Conference contribution
• 26 Article
• 8 Book editing
• 6 Chapter
• 23 More
  • 5 Software
  • 4 Foreword/editorial
  • 3 Phd Thesis 1 (Research TU/e / Graduation TU/e)
  • 3 EngD Thesis
  • 3 Preprint
  • 2 Conference article
  • 1 Report
  • 1 Editorial
  • 1 Working paper

Content available in repository

Content available in repository

Search results

• 2025

  Formal Methods in Industry

  ter Beek, M. H. (Corresponding author), Chapman, R., Cleaveland, R., Garavel, H., Gu, R., ter Horst, I., Keiren, J. J. A., Lecomte, T., Leuschel, M., Rozier, K. Y., Sampaio, A., Seceleanu, C., Thomas, M., Willemse, T. A. C. & Zhang, L., Mar 2025, In: Formal Aspects of Computing. 37, 1, p. 1-38 38 p., 7.

  Research output: Contribution to journal › Article › Academic › peer-review

  Open Access

  File

  • Cloud Security 100%
  8 Citations (Scopus)

  4 Downloads (Pure)

• OIL: an industrial case study in language engineering with Spoofax

  Bunte, O. (Corresponding author), Denkers, J. (Corresponding author), van Gool, L. C. M., Vinju, J. J., Visser, E., Willemse, T. A. C. & Zaidman, A., Feb 2025, In: Software and Systems Modeling. 24, 1, p. 139-182 44 p.

  Research output: Contribution to journal › Article › Academic › peer-review

  Open Access

  File

  • Industrial Case 100%
  • Case Study 100%
  • Domain-specific languages 100%
  • Specific Industry 100%
  • Value Added 50%
  1 Downloads (Pure)

• Unfolding state variables improves model checking performance

  Stramaglia, A., Keiren, J. J. A. (Corresponding author) & Neele, T., 22 May 2025, In: Theoretical Computer Science. 1038, 28 p., 115181.

  Research output: Contribution to journal › Article › Academic › peer-review

  Open Access

  File

  • Model Checking 100%
  • State Variable 100%
  • Complex Data Type 60%
  • Static Program Analysis 40%
  • State Space 20%
• 2024

  Back to the format: A survey on SOS for probabilistic processes

  Castiglioni, V. (Corresponding author), Lanotte, R. & Tini, S., Feb 2024, In: Journal of Logical and Algebraic Methods in Programming. 137, 46 p., 100929.

  Research output: Contribution to journal › Article › Academic › peer-review

  Open Access

  File

  • Qualitative Behavior 100%
  • Closeness 100%
  • Process Algebra 100%
  • Operational Semantics 100%
  • Qualitative Description 100%
  1 Citation (Scopus)

  22 Downloads (Pure)

• Feature causality

  Dubslaff, C. (Corresponding author), Weis, K., Baier, C. & Apel, S., Mar 2024, In: Journal of Systems and Software. 209, 19 p., 111915.

  Research output: Contribution to journal › Article › Academic › peer-review

  Open Access

  File

  • Feature Interaction 100%
  • System Configuration 50%
  • Software Systems 50%
  • Configurable System 50%
  • Nonfunctional Property 50%
  2 Citations (Scopus)

  32 Downloads (Pure)

• Lazy model checking for recursive state machines

  Dubslaff, C. (Corresponding author), Wienhöft, P. (Corresponding author) & Fehnker, A., Apr 2024, In: Software and Systems Modeling. 23, 2, p. 369-401 33 p.

  Research output: Contribution to journal › Article › Academic › peer-review

  Open Access

  File

  • State Machine 100%
  • Model Checking 100%
  • Model Checking Algorithm 60%
  • Computation Tree 40%
  • Procedural Program 40%
  13 Downloads (Pure)

• Negative Latency in the Tactile Internet as Enabler for Global Metaverse Immersion

  Schulz, J., Dubslaff, C., Seeling, P., Li, S. C., Speidel, S. & Fitzek, F. H. P. (Corresponding author), Sept 2024, In: IEEE Network. 38, 5, p. 167-173 7 p., 10466554.

  Research output: Contribution to journal › Article › Academic › peer-review

  Open Access

  File

  • User Interaction 100%
  • Propagation Delay 100%
  • Human Cooperation 100%
  8 Citations (Scopus)

  5 Downloads (Pure)

• Operations on Fixpoint Equation Systems

  Neele, T. & van de Pol, J., 10 Jul 2024, In: Logical Methods in Computer Science. 20, 3, 32 p.

  Research output: Contribution to journal › Article › Academic › peer-review

  Open Access

  File

  • Equation System 100%
  • Complete Lattice 66%
  • Extremal 33%
  14 Downloads (Pure)

• Parameter synthesis for Markov models: covering the parameter space

  Junges, S., Ábrahám, E., Hensel, C., Jansen, N. (Corresponding author), Katoen, J.-P., Quatmann, T. & Volk, M., Jun 2024, In: Formal Methods in System Design. 62, 1-3, p. 181-259 79 p.

  Research output: Contribution to journal › Article › Academic › peer-review

  Open Access

  File

  • Parameter Value 100%
  • Parameter Space 100%
  • Chain Analysis 66%
  • Markov Chain 66%
  • Software Development Tool 33%
  6 Citations (Scopus)

  29 Downloads (Pure)

• XACML2mCRL2: Automatic transformation of XACML policies into mCRL2 specifications

  Arshad, H. (Corresponding author), Horne, R., Johansen, C., Owe, O. & Willemse, T. A. C., Jan 2024, In: Science of Computer Programming. 232, 10 p., 103046.

  Research output: Contribution to journal › Article › Academic › peer-review

  Open Access

  File

  • Access Control Policies 100%
  • Formal Verification 50%
  • Markup Language 25%
  • Access Control 25%
  • Grained Access Control 25%
  19 Downloads (Pure)
• 2023

  A Unifying Formal Approach to Importance Values in Boolean Functions

  Harder, H. (Corresponding author), Jantsch, S., Baier, C. & Dubslaff, C., 14 May 2023, In: arXiv. 2023, 33 p., 2305.08103.

  Research output: Contribution to journal › Article › Academic

  Open Access

  File

  • Boolean Function 100%
  • Importance Value 100%
  • Binary Decision 28%
  • binary decision diagram 28%
  • Central Role 14%
  40 Downloads (Pure)

• Decomposing monolithic processes in a process algebra with multi-actions

  Laveaux, M. (Corresponding author) & Willemse, T. A. C., Apr 2023, In: Journal of Logical and Algebraic Methods in Programming. 132, 24 p., 100858.

  Research output: Contribution to journal › Article › Academic › peer-review

  Open Access

  File

  • State Space 100%
  • Process Algebra 100%
  • Multiple Process 100%
  • Prefixing 100%
  • Resulting Process 100%
  21 Downloads (Pure)

• More for Less: Safe Policy Improvement With Stronger Performance Guarantees

  Wienhöft, P., Suilen, M., Simão, T. D. (Corresponding author), Dubslaff, C., Baier, C. & Jansen, N., 13 Apr 2023, In: arXiv. 2023, 15 p., 2305.07958.

  Research output: Contribution to journal › Article › Academic

  Open Access

  File

  • Performance Guarantee 100%
  • Reinforcement Learning 100%
  • Environment Model 100%
  • Sample Data 100%
  16 Downloads (Pure)

• On the Foundations of Cycles in Bayesian Networks

  Baier, C., Dubslaff, C., Hermanns, H. & Käfer, N., 20 Jan 2023, In: CoRR. abs/2301.08608

  Research output: Contribution to journal › Article › Academic

  • Bayesian Networks 100%
  • Bayesian Network 100%
  • Random Variable 40%
  • Feedback Loop 20%
  • Directed Acyclic Graph 20%

• Real Equation Systems with Alternating Fixed-points (full version with proofs).

  Groote, J. F. & Willemse, T. A. C., 2023, In: CoRR. abs/2307.07455

  Research output: Contribution to journal › Article › Academic
• 2022

  Formal verification of OIL component specifications using mCRL2

  Bunte, O. (Corresponding author), van Gool, L. C. M. (Corresponding author) & Willemse, T. A. C. (Corresponding author), Jun 2022, In: International Journal on Software Tools for Technology Transfer. 24, 3, p. 441-472 32 p.

  Research output: Contribution to journal › Article › Academic › peer-review

  Open Access

  File

  • Formal Verification 100%
  • Model Checking 100%
  • Checking Technique 66%
  • Control Software 33%
  • Software Component 33%
  3 Citations (Scopus)

  129 Downloads (Pure)

• On-The-Fly Solving for Symbolic Parity Games

  Laveaux, M., Wesselink, W. & Willemse, T. A. C., 2022, In: CoRR. abs/2201.09607

  Research output: Contribution to journal › Article › Academic

• Partial-order reduction for parity games and parameterised Boolean equation systems

  Neele, T. (Corresponding author), Willemse, T. A. C., Wesselink, W. & Valmari, A., Oct 2022, In: International Journal on Software Tools for Technology Transfer. 24, 5, p. 735-756 22 p.

  Research output: Contribution to journal › Article › Academic › peer-review

  Open Access

  File

  • Partial Order Reduction 100%
  • Boolean Equation 100%
  • Equation System 100%
  • Model Checking 60%
  • State Space 20%
  3 Citations (Scopus)

  50 Downloads (Pure)
• 2021

  A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction

  Neele, T., Valmari, A. & Willemse, T. A. C., 21 Jul 2021, In: Logical Methods in Computer Science. 17, 3, p. 8:1–8:27 27 p., 8.

  Research output: Contribution to journal › Article › Academic › peer-review

  Open Access

  File

  • Partial Order Reduction 100%
  • Partial Order 100%
  • Model Checking 66%
  • Approximation (Algorithm) 33%
  • State Space 33%
  1 Citation (Scopus)

  55 Downloads (Pure)

• Correct and Efficient Antichain Algorithms for Refinement Checking

  Laveaux, M., Groote, J. F. & Willemse, T. A. C., 2021, In: Logical Methods in Computer Science. 17, 1, 40 p., 8.

  Research output: Contribution to journal › Article › Academic › peer-review

  Open Access

  File

  • Soundness 100%
  • Software Engineering 100%
  • Development Methodology 100%
  1 Citation (Scopus)

  38 Downloads (Pure)
• 2020

  Decompositional Minimisation of Monolithic Processes

  Laveaux, M. & Willemse, T. A. C., 11 Dec 2020, In: arXiv. 2020, 24 p., 2012.06468.

  Research output: Contribution to journal › Article › Academic

  Open Access

  File

  • Parallel Composition 100%
  • Simple Form 100%
  • State Space 50%
  • Sequential Process 50%
  • Static Program Analysis 50%
  19 Downloads (Pure)
• 2019

  Breaking the Limits of Redundancy Systems Analysis

  Dubslaff, C., Ding, K., Morozov, A., Baier, C. & Janschek, K., 2019, In: CoRR. abs/1912.05364

  Research output: Contribution to journal › Article › Academic
• 2018

  Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic Büchi automata

  Klein, J., Baier, C., Chrszon, P., Daum, M., Dubslaff, C., Klüppelholz, S., Märcker, S. & Müller, D., 2018, In: International Journal on Software Tools for Technology Transfer. 20, 2, p. 179-194 16 p., 2.

  Research output: Contribution to journal › Article › Academic › peer-review
  26 Citations (Scopus)

• From verification to synthesis under cost-utility constraints

  Baier, C. & Dubslaff, C., 2018, In: ACM SIGLOG News. 5, 4, p. 26-46 21 p., 4.

  Research output: Contribution to journal › Article › Academic › peer-review

• ProFeat: feature-oriented engineering for family-based probabilistic model checking

  Chrszon, P., Dubslaff, C., Klüppelholz, S. & Baier, C., 2018, In: Formal Aspects of Computing. 30, 1, p. 45-75 31 p., 1.

  Research output: Contribution to journal › Article › Academic › peer-review
  62 Citations (Scopus)
• 2012

  Model checking probabilistic systems against pushdown specifications

  Dubslaff, C., Baier, C. & Berg, M., 2012, In: Information Processing Letters. 112, 8-9, p. 320-328 9 p., 8-9.

  Research output: Contribution to journal › Article › Academic › peer-review
  4 Citations (Scopus)