A framework for compositional verification of multi-valued systems via abstraction-refinement
From MaRDI portal
Publication:259065
DOI10.1016/j.ic.2016.01.001zbMath1336.68166OpenAlexW2264857910MaRDI QIDQ259065
Orna Grumberg, Sharon Shoham, Yael Meller
Publication date: 10 March 2016
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2016.01.001
refinementbilatticescompositional model checkingmixed simulationmu-calculusmulti-valued model checking
Cites Work
- Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning
- Automated assumption generation for compositional verification
- Automatic symbolic compositional verification by learning assumptions
- When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus
- A lattice-theoretical fixpoint theorem and its applications
- Latticed Simulation Relations and Games
- Automated Assume-Guarantee Reasoning by Abstraction Refinement
- Compositional Verification and 3-Valued Abstractions Join Forces
- Learning Minimal Separating DFA’s for Compositional Verification
- A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement
- Algebraic Methodology and Software Technology
- SAT-Based Compositional Verification Using Lazy Learning
- Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
- Automata, Languages and Programming
- Automated Technology for Verification and Analysis
- Verification, Model Checking, and Abstract Interpretation
- Computer Aided Verification
- Computer Aided Verification
- Refining Interface Alphabets for Compositional Verification
- Optimized L*-Based Assume-Guarantee Reasoning
- Verification, Model Checking, and Abstract Interpretation
- Tools and Algorithms for the Construction and Analysis of Systems
- CONCUR 2003 - Concurrency Theory
- Computer Aided Verification
- 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
