Combining partial-order reductions with on-the-fly model-checking.
From MaRDI portal
Publication:960506
DOI10.1007/BF00121262zbMath1425.68267OpenAlexW1965309410MaRDI QIDQ960506
Publication date: 21 December 2008
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00121262
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items
Stubborn set reduction for timed reachability and safety games, Model checking \(\omega \)-regular properties with decoupled search, Stutter-invariant temporal properties are expressible without the next-time operator, Partial-Order Reduction, Multithreaded testing of program interfaces, An application of temporal projection to interleaving concurrency, Verifying a signature architecture: a comparative case study, Unnamed Item, Partial-order reduction in the weak modal mu-calculus, An algorithmic approach for checking closure properties of Ω-regular languages, Exponential automatic amortized resource analysis, The inconsistent labelling problem of stutter-preserving partial-order reduction, Transparent partial order reduction, An automatic method for the dynamic construction of abstractions of states of a formal model, Boosting Lazy Abstraction for SystemC with Partial Order Reduction, Formal verification of an executable LTL model checker with partial order reduction, Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems, Ensuring completeness of symbolic verification methods for infinite-state systems, On stubborn sets in the verification of linear time temporal properties, From LCF to Isabelle/HOL, Survey on Directed Model Checking, An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages, Specification Languages for Stutter-Invariant Regular Properties, Unnamed Item
Cites Work
- Event fairness and non-interleaving concurrency
- Appraising fairness in languages for distributed programming
- Defining conditional independence using collapses
- Proving partial order properties
- Propositional dynamic logic of looping and converse is elementarily decidable
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Unnamed Item
- Unnamed Item
