Symbolic model checking with rich assertional languages

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)

zbMATH Keywords

regular expressions; parametric systems; symbolic model checking; tree automata

Mathematics Subject Classification ID

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, Unnamed Item, 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), Checking deadlock-freedom of parametric component-based systems, View abstraction for systems with component identities, Computable fixpoints in well-structured symbolic model checking, A novel approach to verifying context free properties of programs, 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, Monitoring Metric First-Order Temporal Properties, Automated formal analysis and verification: an overview, AUTOMATIC VERIFICATION OF DIRECTORY-BASED CONSISTENCY PROTOCOLS WITH GRAPH CONSTRAINTS, Model Checking Parameterized Systems, 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

• MONA
• CESAR

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