Abstraction and Abstraction Refinement
From MaRDI portal
Publication:3176371
DOI10.1007/978-3-319-10575-8_13zbMath1392.68244OpenAlexW2803191666MaRDI QIDQ3176371
Publication date: 20 July 2018
Published in: Handbook of Model Checking (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-10575-8_13
Related Items
Explicit-State Model Checking, Compositional Reasoning, Interpolation and Model Checking, Predicate Abstraction for Program Verification, Combining Model Checking and Deduction, Process Algebra and Model Checking, Simulation relations and applications in formal methods
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Data structures for symbolic multi-valued model-checking
- 3-valued abstraction: More precision at less cost
- Extensional equivalences for transition systems
- Characterizing finite Kripke structures in propositional temporal logic
- Property preserving abstractions for the verification of concurrent systems
- Verification by augmented finitary abstraction
- Predicate abstraction of ANSI-C programs using SAT
- When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus
- Temporal Logic and Fair Discrete Systems
- Modeling for Verification
- BDD-Based Symbolic Model Checking
- SAT-Based Model Checking
- Predicate Abstraction for Program Verification
- The mu-calculus and Model Checking
- Abstractions from proofs
- Counterexample-guided abstraction refinement for symbolic model checking
- 3-Valued Circuit SAT for STE with Automatic Refinement
- Automated Assume-Guarantee Reasoning by Abstraction Refinement
- Abstraction and Refinement in Model Checking
- Compositional Verification and 3-Valued Abstractions Join Forces
- A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement
- Algebraic laws for nondeterminism and concurrency
- Three logics for branching bisimulation
- Temporal abstract interpretation
- Lazy abstraction
- Simulation-based minimization
- A game-based framework for CTL counterexamples and 3-valued abstraction-refinement
- Tools and Algorithms for the Construction and Analysis of Systems
- Predicate Abstraction via Symbolic Decision Procedures
- Array Abstractions from Proofs
- Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
- Efficient Automatic STE Refinement Using Responsibility
- Automata, Languages and Programming
- Static Analysis
- Automated Technology for Verification and Analysis
- Formal Methods in Computer-Aided Design
- Tools and Algorithms for the Construction and Analysis of Systems
- Verification, Model Checking, and Abstract Interpretation
- Computer Aided Verification
- Automatic Refinement and Vacuity Detection for Symbolic Trajectory Evaluation
- Lazy Abstraction with Interpolants
- Optimized L*-Based Assume-Guarantee Reasoning
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
