Symbolic model checking with rich assertional languages
From MaRDI portal
Recommendations
Cites work
- A structural induction theorem for processes
- An experience in proving regular networks of processes by modular model checking
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Automatic verification of parameterized networks of processes
- Branching-time temporal logic and tree automata
- Generalized finite automata theory with an application to a decision problem of second-order logic
- scientific article; zbMATH DE number 3854429 (Why is no real title available?)
- scientific article; zbMATH DE number 3757688 (Why is no real title available?)
- scientific article; zbMATH DE number 52331 (Why is no real title available?)
- scientific article; zbMATH DE number 789389 (Why is no real title available?)
- Interpolants and Symbolic Model Checking
- On Reasoning About Rings
- Reasoning about networks with many identical finite state processes
- Reasoning about systems with many processes
- Symbolic model checking: \(10^{20}\) states and beyond
- Tree acceptors and some of their applications
- Using branching time temporal logic to synthesize synchronization skeletons
Cited in
(56)- 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
- Symbolic model checking: \(10^{20}\) states and beyond
- A symbolic semantics for abstract model checking
- 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
- Computing parameterized invariants of parameterized Petri nets
- Regular model checking with regular relations
- 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
- Verification of component-based systems with recursive architectures
- Monitoring metric first-order temporal properties
- Model checking for symbolic-heap separation logic with inductive predicates
- Automated formal analysis and verification: an overview
- Automatic verification of directory-based consistency protocols with graph constraints
- Model checking parameterized systems
- Symbolic model checking in non-Boolean domains
- Model Checking MSVL Programs Based on Dynamic Symbolic Execution
- BISIMULATION MINIMIZATION OF TREE AUTOMATA
- Monotonic Abstraction for Programs with Dynamic Memory Heaps
- Symbolic model checking of actor-oriented high-level SystemC models with interval diagrams
- Towards SMT Model Checking of Array-Based Systems
- AlPiNA: A Symbolic Model Checker
- MONOTONIC ABSTRACTION: ON EFFICIENT VERIFICATION OF PARAMETERIZED SYSTEMS
- Automatic Verification of Directory-Based Consistency Protocols
- Verification of graph grammars using a logical approach
- Exploiting step semantics for efficient bounded model checking of asynchronous systems
- scientific article; zbMATH DE number 1796141 (Why is no real title available?)
- scientific article; zbMATH DE number 2102716 (Why is no real title available?)
- 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 (preliminary results)
- Networks of processes with parameterized state space
- Monotonic abstraction in parameterized verification
- Structural Invariants for the Verification of Systems with Parameterized Architectures
- Computing Parameterized Invariants of Parameterized Petri Nets
- View abstraction -- a tutorial (invited paper)
- Model Checking Software
- 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
- Regular model checking: evolution and perspectives
- Parameterized verification under TSO with data types
- On complementation of nondeterministic finite automata without full determinization
- Computing inductive invariants of regular abstraction frameworks
- Modular derivation of decision procedures for extensions of the algebraic theory of arrays
- Action language verifier: An infinite-state model checker for reactive software specifications
- Permutation rewriting and algorithmic verification
- CSL model checking algorithms for QBDs
This page was built for publication: Symbolic model checking with rich assertional languages
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5941102)
