An efficient approach for abstraction-refinement in model checking

DOI10.1016/J.TCS.2011.12.014MaRDI QIDQ690465zbMATH OpenOpenAlexFDO

Authors Cong Tian, Zhenhua Duan, 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

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)

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

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1956580 (Why is no real title available?)
• scientific article; zbMATH DE number 1979542 (Why is no real title available?)
• scientific article; zbMATH DE number 1903358 (Why is no real title available?)
• DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC
• Integrating Evolutionary Computation with Abstraction Refinement for Model Checking
• Lazy abstraction
• Semantical Analysis of Modal Logic I Normal Modal Propositional Calculi
• The complexity of verification

Cited in

(17)

• Concrete abstractions. Formalizing and analyzing discrete theories and algorithms with the RISCAL model checker
• Exploiting design structure in model checking. (Abstract)
• Automata-Based Abstraction Refinement for µHORS Model Checking
• Combining search space partition and abstraction for LTL model checking
• Tools and Algorithms for the Construction and Analysis of Systems
• scientific article; zbMATH DE number 1948409 (Why is no real title available?)
• Abstraction refinement for emptiness checking of alternating data automata
• A type-directed abstraction refinement approach to higher-order model checking
• scientific article; zbMATH DE number 1863177 (Why is no real title available?)
• scientific article; zbMATH DE number 1903350 (Why is no real title available?)
• Computer Aided Verification
• Correct Hardware Design and Verification Methods
• Making abstraction-refinement efficient in model checking
• Abstraction and Refinement in Model Checking
• An Efficient Equivalence-checking Algorithm for a Model of Programs with Commutative and Absorptive Statements
• Model Checking Software
• scientific article; zbMATH DE number 1979542 (Why is no real title available?)

Describes a project that uses

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)