Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
From MaRDI portal
Publication:1910794
DOI10.1007/3-540-60761-7zbMath1293.68005OpenAlexW2093709900MaRDI QIDQ1910794
Publication date: 20 March 1996
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-60761-7
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Research exposition (monographs, survey articles) pertaining to computer science (68-02)
Related Items
A geometric view of partial order reduction ⋮ Topological abstraction of higher-dimensional automata ⋮ Compact and efficiently verifiable models for concurrent systems ⋮ Stubborn set reduction for timed reachability and safety games ⋮ Stateless model checking under a reads-value-from equivalence ⋮ Model checking \(\omega \)-regular properties with decoupled search ⋮ Stubborn versus structural reductions for Petri nets ⋮ Model Checking Concurrent Programs ⋮ Combining Model Checking and Testing ⋮ Delay-dependent partial order reduction technique for real time systems ⋮ Partial Order Reduction for Probabilistic Systems: A Revision for Distributed Schedulers ⋮ Optimistic synchronization-based state-space reduction ⋮ \(\text{DELFIN}^+\): an efficient deadlock detection tool for CCS processes ⋮ Question-guided stubborn set methods for state properties ⋮ Multithreaded testing of program interfaces ⋮ POR for security protocol equivalences. Beyond action-determinism ⋮ An application of temporal projection to interleaving concurrency ⋮ Stateless model checking for TSO and PSO ⋮ Modular discrete time approximations of distributed hybrid automata ⋮ Independence Abstractions and Models of Concurrency ⋮ Dynamic Reductions for Model Checking Concurrent Software ⋮ Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions ⋮ Producing Short Counterexamples Using “Crucial Events” ⋮ Exponential automatic amortized resource analysis ⋮ The inconsistent labelling problem of stutter-preserving partial-order reduction ⋮ From hidden to visible: a unified framework for transforming behavioral theories into rewrite theories ⋮ TASS: the toolkit for accurate scientific software ⋮ Techniques and applications of computation slicing ⋮ Transparent partial order reduction ⋮ Folded Hasse diagrams of combined traces ⋮ Succinct discrete time approximations of distributed hybrid automata ⋮ Accurate hybridization of nonlinear systems ⋮ Compositional analysis for linear control systems ⋮ On integration of event-based estimation and robust MPC in a feedback loop ⋮ From synchronous programs to symbolic representations of hybrid systems ⋮ A descent algorithm for the optimal control of constrained nonlinear switched dynamical systems ⋮ Timed automata with observers under energy constraints ⋮ Real-time scheduling of mixture-of-experts systems with limited resources ⋮ On a control algorithm for time-varying processor availability ⋮ Timed I/O automata ⋮ Receding horizon control for temporal logic specifications ⋮ Synthesis using approximately bisimilar abstractions ⋮ Oscillation analysis of linearly coupled piecewise affine systems ⋮ On infinity norms as Lyapunov functions for piecewise affine systems ⋮ Identifiability of discrete-time linear switched systems ⋮ Rank properties of poincare maps for hybrid systems with applications to bipedal walking ⋮ Stealthy deception attacks on water SCADA systems ⋮ Comparison of overapproximation methods for stability analysis of networked control systems ⋮ Distributed Kalman Filter algorithms for self-localization of mobile devices ⋮ Convergence results for ant routing algorithms viastochastic approximation ⋮ Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems ⋮ Automatic invariant generation for hybrid systems using ideal fixed points ⋮ Safe compositional network sketches ⋮ Bayesian statistical model checking with application to Simulink/Stateflow verification ⋮ On the connections between PCTL and dynamic programming ⋮ Modeling and verification of stochastic hybrid systems using HIOA ⋮ A generating function approach to the stability of discrete-time switched linear systems ⋮ Stabilization of planar switched linear systems using polar coordinates ⋮ Amir Pnueli and the dawn of hybrid systems ⋮ Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions ⋮ Dynamic Partial Order Reduction Using Probe Sets ⋮ An automatic method for the dynamic construction of abstractions of states of a formal model ⋮ A comparison of confluence and ample sets in probabilistic and non-probabilistic branching time ⋮ Analysis of correct synchronization of operating system components ⋮ Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs ⋮ Boosting Lazy Abstraction for SystemC with Partial Order Reduction ⋮ Model checking properties on reduced trace systems ⋮ Confluence reduction for Markov automata ⋮ Partial order reduction for checking soundness of time workflow nets ⋮ On the Origin of Events: Branching Cells as Stubborn Sets ⋮ Component-wise incremental LTL model checking ⋮ Star-topology decoupled state space search ⋮ Partial-order Boolean games: informational independence in a logic-based model of strategic interaction ⋮ Event clock message passing automata: a logical characterization and an emptiness checking algorithm ⋮ Ant colony optimization with partial order reduction for discovering safety property violations in concurrent models ⋮ Hard real-time tasks' scheduling considering voltage scaling, precedence and exclusion relations ⋮ On commutativity based edge lean search ⋮ Composing model programs for analysis ⋮ Difficult configurations -- on the complexity of LTrL ⋮ On stubborn sets in the verification of linear time temporal properties ⋮ Abstract reduction in directed model checking CCS processes ⋮ Approximate partial order reduction ⋮ Dynamical modeling and analysis of large cellular regulatory networks ⋮ Compositional analysis of C/C++ programs with veriSoft ⋮ Dynamic Path Reduction for Software Model Checking ⋮ An expressively complete linear time temporal logic for Mazurkiewicz traces ⋮ Optimising the ProB model checker for B using partial order reduction ⋮ Collective Assertions ⋮ Quasi-optimal partial order reduction ⋮ Full simulation coverage for SystemC transaction-level models of systems-on-a-chip ⋮ Using formal verification to evaluate the execution time of Spark applications ⋮ Using heuristic search for finding deadlocks in concurrent systems ⋮ A partial order semantics approach to the clock explosion problem of timed automata ⋮ More efficient on-the-fly LTL verification with Tarjan's algorithm ⋮ Partial Order Reduction for Rewriting Semantics of Programming Languages ⋮ Pomset bisimulation and unfolding for reset Petri nets ⋮ Translating Java for multiple model checkers: The Bandera back-end ⋮ Reduced models for efficient CCS verification ⋮ Control of safe ordinary Petri nets using unfolding ⋮ Efficient abstraction algorithms for predicate detection ⋮ Star-Topology Decoupling in SPIN ⋮ Weak equivalence of higher-dimensional automata ⋮ Model Checking Linear-Time Properties of Probabilistic Systems ⋮ Unnamed Item ⋮ A product version of dynamic linear time temporal logic ⋮ A pragmatic approach to stateful partial order reduction ⋮ Unfolding-based dynamic partial order reduction of asynchronous distributed programs ⋮ Partial-Order Reduction for Parity Games with an Application on Parameterised Boolean Equation Systems ⋮ Formal Verification of Concurrent Systems via Directed Model Checking ⋮ Covering Steps Graphs of Time Petri Nets ⋮ The tool TINA – Construction of abstract state spaces for petri nets and time petri nets ⋮ Testing Distributed Systems Through Symbolic Model Checking ⋮ Survey on Directed Model Checking ⋮ Interprocedural Analysis of Concurrent Programs Under a Context Bound ⋮ A Reduction Theorem for the Verification of Round-Based Distributed Algorithms ⋮ Exploring the Scope for Partial Order Reduction ⋮ Stubborn Sets, Frozen Actions, and Fair Testing ⋮ Unnamed Item ⋮ Property-oriented expansion
