Symbolic model checking with rich assertional languages
From MaRDI portal
Publication:5941102
DOI10.1016/S0304-3975(00)00103-1zbMath0973.68119MaRDI QIDQ5941102
No author found.
Publication date: 20 August 2001
Published in: Theoretical Computer Science (Search for Journal in Brave)
Related Items (41)
Structural Invariants for the Verification of Systems with Parameterized Architectures ⋮ Computing Parameterized Invariants of Parameterized Petri Nets ⋮ Model checking and abstraction to the aid of parameterized systems (a survey) ⋮ Regular model checking with regular relations ⋮ Model Checking Parameterized Systems ⋮ Permutation rewriting and algorithmic verification ⋮ Unnamed Item ⋮ Regular model checking: evolution and perspectives ⋮ BISIMULATION MINIMIZATION OF TREE AUTOMATA ⋮ Monotonic Abstraction for Programs with Dynamic Memory Heaps ⋮ Verification of graph grammars using a logical approach ⋮ Exploiting step semantics for efficient bounded model checking of asynchronous systems ⋮ Verification of component-based systems with recursive architectures ⋮ Towards SMT Model Checking of Array-Based Systems ⋮ AUTOMATIC VERIFICATION OF DIRECTORY-BASED CONSISTENCY PROTOCOLS WITH GRAPH CONSTRAINTS ⋮ Computable fixpoints in well-structured symbolic model checking ⋮ Checking deadlock-freedom of parametric component-based systems ⋮ Verification of parametric concurrent systems with prioritised FIFO resource management ⋮ Regular Model Checking using Widening Techniques ⋮ Verifying a Network Invariant for All Configurations of the Futurebus+ Cache Coherence Protocol ⋮ An Assertional Language for the Verification of Systems Parametric in Several Dimensions ⋮ Networks of Processes with Parameterized State Space ⋮ Automatic verification of parameterized networks of processes ⋮ Ensuring completeness of symbolic verification methods for infinite-state systems ⋮ Tree regular model checking: a simulation-based approach ⋮ View abstraction for systems with component identities ⋮ CSL model checking algorithms for QBDs ⋮ Monitoring Metric First-Order Temporal Properties ⋮ Handling Parameterized Systems with Non-atomic Global Conditions ⋮ A novel approach to verifying context free properties of programs ⋮ On Verifying Fault Tolerance of Distributed Protocols ⋮ Monotonic Abstraction in Parameterized Verification ⋮ Don't care words with an application to the automata-based approach for real addition ⋮ MONOTONIC ABSTRACTION: ON EFFICIENT VERIFICATION OF PARAMETERIZED SYSTEMS ⋮ Automatic Verification of Directory-Based Consistency Protocols ⋮ Approximated parameterized verification of infinite-state processes with global conditions ⋮ Monotonic Abstraction in Action ⋮ Decidable first-order transition logics for PA-processes ⋮ Iterating transducers ⋮ Automated formal analysis and verification: an overview ⋮ Computing parameterized invariants of parameterized Petri nets
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Reasoning about networks with many identical finite state processes
- Using branching time temporal logic to synthesize synchronization skeletons
- Symbolic model checking: \(10^{20}\) states and beyond
- An experience in proving regular networks of processes by modular model checking
- A structural induction theorem for processes
- Branching-time temporal logic and tree automata
- Tree acceptors and some of their applications
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Reasoning about systems with many processes
- Interpolants and Symbolic Model Checking
- Generalized finite automata theory with an application to a decision problem of second-order logic
- On Reasoning About Rings
- Automatic verification of parameterized networks of processes
This page was built for publication: Symbolic model checking with rich assertional languages
