Unfolding state variables improves model checking performance

DOI10.1016/J.TCS.2025.115181MaRDI QIDQ7001144zbMATH OpenFDO

Authors Anna Stramaglia, Jeroen J. A. Keiren, Thomas Neele

Publication date 7 April 2025

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.TCS.2025.115181

zbMATH Keywords

algebraic data typesmodel checkingprocess algebrastatic analysis

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites work

• An axiomatic basis for computer programming
• BI as an assertion language for mutable data structures
• Data flow analysis as model checking
• FDR3 -- a modern refinement checker for CSP
• Foundations of algebraic specification and formal software development.
• Horn clause solvers for program verification
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 3716792 (Why is no real title available?)
• scientific article; zbMATH DE number 1796138 (Why is no real title available?)
• scientific article; zbMATH DE number 7269247 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• Lectures on Petri nets. 1: Basic models. Advances in Petri nets
• Liveness analysis for parameterised Boolean equation systems
• Model checking
• Modeling and analysis of communicating systems
• Parameterised Boolean equation systems
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Process algebra: equational theories of communicating processes. With forewords by Tony Hoare, Robin Milner and Jan Bergstra.
• Simplifying process parameters by unfolding algebraic data types
• State space reduction for process algebra specifications
• State space reduction of linear processes using control flow reconstruction
• Static Analysis Techniques for Parameterised Boolean Equation Systems
• Structured algebraic specifications: A kernel language
• Symbolic model checking: \(10^{20}\) states and beyond
• Symbolic Reachability for Process Algebras with Recursive Data Types
• The algebraic specification of abstract data types

This page was built for publication: Unfolding state variables improves model checking performance

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7001144)