Data structures for symbolic multi-valued model-checking
From MaRDI portal
Publication:862857
DOI10.1007/s10703-006-0016-zzbMath1109.68063OpenAlexW2059949763MaRDI QIDQ862857
Benet Devereux, Steve Easterbrook, Marsha Chechik, Albert Lai, Arie Gurfinkel
Publication date: 24 January 2007
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-006-0016-z
Logic in artificial intelligence (68T27) Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05) Many-valued logic (03B50)
Related Items (20)
Integrating Topological Proofs with Model Checking to Instrument Iterative Design ⋮ Statistical Model Checking for Variability-Intensive Systems ⋮ Abstraction and Abstraction Refinement ⋮ Data structures for symbolic multi-valued model-checking ⋮ Fuzzy Halpern and Shoham's interval temporal logics ⋮ Model checking computation tree logic over finite lattices ⋮ Multi-valued model checking games ⋮ Quantitative model checking of linear-time properties based on generalized possibility measures ⋮ Symbolic checking of fuzzy CTL on fuzzy program graph ⋮ Computation tree logic model checking based on multi-valued possibility measures ⋮ A Direct Algorithm for Multi-valued Bounded Model Checking ⋮ Model checking fuzzy computation tree logic ⋮ Multi-robot LTL planning under uncertainty ⋮ Model checking of linear-time properties in multi-valued systems ⋮ TOrPEDO : witnessing model correctness with topological proofs ⋮ Statistical model checking for variability-intensive systems: applications to bug detection and minimization ⋮ A verification-driven framework for iterative design of controllers ⋮ Quantitative \(\mu\)-calculus and CTL defined over constraint semirings ⋮ Simulation for lattice-valued doubly labeled transition systems ⋮ Abstraction and approximation in fuzzy temporal logics and models
Uses Software
Cites Work
- Data structures for symbolic multi-valued model-checking
- Automatic verification of finite-state concurrent systems using temporal logic specifications
- Graph-Based Algorithms for Boolean Function Manipulation
- Binary Decision Diagrams
- Model checking lattices: using and reasoning about information orders for abstraction
- Branching Programs and Binary Decision Diagrams
- Tools and Algorithms for the Construction and Analysis of Systems
- Computer Aided Verification
- Computer Aided Verification
- Verification, Model Checking, and Abstract Interpretation
- CONCUR 2003 - Concurrency Theory
- Computer Aided Verification
- Efficient detection of vacuity in temporal model checking
- SCTL-MUS: A formal methodology for software development of distributed systems. A case study
- 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
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Data structures for symbolic multi-valued model-checking
