Symbolic model checking with rich assertional languages
From MaRDI portal
Recommendations
Cites work
- 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?)
- 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
- 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
(55)- A symbolic semantics for abstract model checking
- MONOTONIC ABSTRACTION: ON EFFICIENT VERIFICATION OF PARAMETERIZED SYSTEMS
- Iterating transducers
- Decidable first-order transition logics for PA-processes
- Model checking for symbolic-heap separation logic with inductive predicates
- Permutation rewriting and algorithmic verification
- Checking deadlock-freedom of parametric component-based systems
- Symbolic model checking of actor-oriented high-level SystemC models with interval diagrams
- scientific article; zbMATH DE number 1796141 (Why is no real title available?)
- Action language verifier: An infinite-state model checker for reactive software specifications
- Verifying a network invariant for all configurations of the Futurebus+ cache coherence protocol
- Symbolic model checking: \(10^{20}\) states and beyond
- Verification of parametric concurrent systems with prioritised FIFO resource management
- CSL model checking algorithms for QBDs
- Exploiting step semantics for efficient bounded model checking of asynchronous systems
- Verification of graph grammars using a logical approach
- Automatic Verification of Directory-Based Consistency Protocols
- View abstraction for systems with component identities
- Automated formal analysis and verification: an overview
- Model checking and abstraction to the aid of parameterized systems (a survey)
- Computing parameterized invariants of parameterized Petri nets
- Regular model checking using widening techniques
- Towards SMT Model Checking of Array-Based Systems
- Regular model checking with regular relations
- Tree regular model checking: a simulation-based approach
- Don't care words with an application to the automata-based approach for real addition
- Monitoring metric first-order temporal properties
- Verification of component-based systems with recursive architectures
- Ensuring completeness of symbolic verification methods for infinite-state systems
- Handling Parameterized Systems with Non-atomic Global Conditions
- Automatic verification of directory-based consistency protocols with graph constraints
- Monotonic Abstraction in Action
- On complementation of nondeterministic finite automata without full determinization
- Computing inductive invariants of regular abstraction frameworks
- Monotonic abstraction in parameterized verification
- On Verifying Fault Tolerance of Distributed Protocols
- Regular model checking: evolution and perspectives
- Parameterized verification under TSO with data types
- Model checking parameterized systems
- scientific article; zbMATH DE number 2102716 (Why is no real title available?)
- Monotonic Abstraction for Programs with Dynamic Memory Heaps
- BISIMULATION MINIMIZATION OF TREE AUTOMATA
- An assertional language for the verification of systems parametric in several dimensions (preliminary results)
- Structural Invariants for the Verification of Systems with Parameterized Architectures
- Computable fixpoints in well-structured symbolic model checking
- A novel approach to verifying context free properties of programs
- AlPiNA: A Symbolic Model Checker
- Networks of processes with parameterized state space
- Automatic verification of parameterized networks of processes
- Model Checking MSVL Programs Based on Dynamic Symbolic Execution
- Approximated parameterized verification of infinite-state processes with global conditions
- Model Checking Software
- scientific article; zbMATH DE number 7121861 (Why is no real title available?)
- Symbolic model checking in non-Boolean domains
- Computing Parameterized Invariants of Parameterized Petri Nets
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)
