An efficient approach for abstraction-refinement in model checking

DOI10.1016/J.TCS.2011.12.014zbMATH Open1252.68197OpenAlexW2069919327MaRDI QIDQ690465FDOQ690465

Zhenhua Duan, Cong Tian, Nan Zhang

Publication date: 27 November 2012

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2011.12.014

Recommendations

• Making abstraction-refinement efficient in model checking
• The abstraction-refinement framework in model checking
• Abstraction and Refinement in Model Checking
• A satisfiability-based approach to abstraction refinement in model checking
• Computer Aided Verification
• Refining and compressing abstract model checking
• Automated Technology for Verification and Analysis
• scientific article; zbMATH DE number 2110619
• Combining Abstraction Refinement and SAT-Based Model Checking

zbMATH Keywords

algorithmmodel checkingabstractionrefinementformal verification

Mathematics Subject Classification ID

Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Title not available (Why is that?)
• Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
• Lazy abstraction
• Integrating Evolutionary Computation with Abstraction Refinement for Model Checking
• The complexity of verification
• DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (15)

• Abstraction refinement for emptiness checking of alternating data automata
• Title not available (Why is that?)
• Title not available (Why is that?)
• Exploiting design structure in model checking. (Abstract)
• Title not available (Why is that?)
• Automata-Based Abstraction Refinement for µHORS Model Checking
• Combining search space partition and abstraction for LTL model checking
• Computer Aided Verification
• Model Checking Software
• Abstraction and Refinement in Model Checking
• Concrete abstractions. Formalizing and analyzing discrete theories and algorithms with the RISCAL model checker
• An Efficient Equivalence-checking Algorithm for a Model of Programs with Commutative and Absorptive Statements
• Title not available (Why is that?)
• Tools and Algorithms for the Construction and Analysis of Systems
• A type-directed abstraction refinement approach to higher-order model checking

Uses Software

• CESAR

This page was built for publication: An efficient approach for abstraction-refinement in model checking

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q690465)