Combining partial-order reductions with on-the-fly model-checking.

model checking temporal logic traces[https://portal.mardi4nfdi.de/w/index.php?title=+Special%3ASearch&search=B%EF%BF%BD%EF%BF%BDchi+automaton&go=Go B��chi automaton]partial-order reduction

Mathematics Subject Classification ID

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)

Cites Work

Title not available (Why is that?)
Title not available (Why is that?)
Propositional dynamic logic of looping and converse is elementarily decidable
Automatic verification of finite-state concurrent systems using temporal logic specifications
Appraising fairness in languages for distributed programming
Event fairness and non-interleaving concurrency
Proving partial order properties
Defining conditional independence using collapses

Cited In (32)

Formal verification of an executable LTL model checker with partial order reduction
Model checking \(\omega \)-regular properties with decoupled search
Stubborn set reduction for timed reachability and safety games
Dynamic partial-order reduction for model checking software
Partial-Order Reduction
Title not available (Why is that?)
Survey on Directed Model Checking
Verifying a signature architecture: a comparative case study
Partial-order reduction in the weak modal mu-calculus
Title not available (Why is that?)
An automatic method for the dynamic construction of abstractions of states of a formal model
Stutter-invariant temporal properties are expressible without the next-time operator
An efficient partial order reduction algorithm with an alternative proviso implementation
Exponential automatic amortized resource analysis
Transparent partial order reduction
Optimising the ProB model checker for B using partial order reduction
An algorithmic approach for checking closure properties of Ω-regular languages
Multithreaded testing of program interfaces
Ensuring completeness of symbolic verification methods for infinite-state systems
An algorithmic approach for checking closure properties of temporal logic specifications and \(\omega\)-regular languages
Title not available (Why is that?)
Finding Stubborn Sets of Coloured Petri Nets without Unfolding
From LCF to Isabelle/HOL
Partially Bounded Context-Aware Verification
Boosting Lazy Abstraction for SystemC with Partial Order Reduction
On Stubborn Sets in the Verification of Linear Time Temporal Properties
An application of temporal projection to interleaving concurrency
On stubborn sets in the verification of linear time temporal properties
Title not available (Why is that?)
Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems
The inconsistent labelling problem of stutter-preserving partial-order reduction
Specification Languages for Stutter-Invariant Regular Properties

This page was built for publication: Combining partial-order reductions with on-the-fly model-checking.

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