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)
68Q45: Formal languages and automata
Related Items
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, Monotonic Abstraction in Parameterized Verification, Handling Parameterized Systems with Non-atomic Global Conditions, On Verifying Fault Tolerance of Distributed Protocols, Monotonic Abstraction in Action, Automatic verification of parameterized networks of processes, Ensuring completeness of symbolic verification methods for infinite-state systems, Verification of graph grammars using a logical approach, Exploiting step semantics for efficient bounded model checking of asynchronous systems, Permutation rewriting and algorithmic verification, CSL model checking algorithms for QBDs, Don't care words with an application to the automata-based approach for real addition, Approximated parameterized verification of infinite-state processes with global conditions, Iterating transducers, Model checking and abstraction to the aid of parameterized systems (a survey), Computable fixpoints in well-structured symbolic model checking, Verification of parametric concurrent systems with prioritised FIFO resource management, Tree regular model checking: a simulation-based approach, Decidable first-order transition logics for PA-processes, Automated formal analysis and verification: an overview, AUTOMATIC VERIFICATION OF DIRECTORY-BASED CONSISTENCY PROTOCOLS WITH GRAPH CONSTRAINTS, BISIMULATION MINIMIZATION OF TREE AUTOMATA, Monotonic Abstraction for Programs with Dynamic Memory Heaps, Towards SMT Model Checking of Array-Based Systems, MONOTONIC ABSTRACTION: ON EFFICIENT VERIFICATION OF PARAMETERIZED SYSTEMS, Automatic Verification of Directory-Based Consistency Protocols
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
