Refining and compressing abstract model checking

DOI10.1016/S1571-0661(04)00151-3MaRDI QIDQ4923520zbMATH OpenFDO

Authors Agostino Dovier, Roberto Giacobazzi, Elisa Quintarelli

Publication date 24 May 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S1571-0661(04)00151-3

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 2110619
• scientific article; zbMATH DE number 1948409
• scientific article; zbMATH DE number 898449
• Abstraction and Refinement in Model Checking
• Generalized Strong Preservation by Abstract Interpretation

Cites work

• scientific article; zbMATH DE number 47903 (Why is no real title available?)
• scientific article; zbMATH DE number 1487860 (Why is no real title available?)
• scientific article; zbMATH DE number 194916 (Why is no real title available?)
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Grammar semantics, analysis and parsing by abstract interpretation
• Optimal domains for disjunctive abstract interpretation
• Refining and compressing abstract domains
• Systematic design of program transformation frameworks by abstract interpretation
• Temporal abstract interpretation

Cited in

(13)

• A type-directed abstraction refinement approach to higher-order model checking
• Abstraction refinement for emptiness checking of alternating data automata
• An efficient approach for abstraction-refinement in model checking
• scientific article; zbMATH DE number 1796131 (Why is no real title available?)
• scientific article; zbMATH DE number 1903350 (Why is no real title available?)
• scientific article; zbMATH DE number 1903381 (Why is no real title available?)
• scientific article; zbMATH DE number 1948409 (Why is no real title available?)
• Computer Aided Verification
• Constraint-based abstract semantics for temporal logic: a direct approach to design and implementation
• Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic
• Concrete abstractions. Formalizing and analyzing discrete theories and algorithms with the RISCAL model checker
• scientific article; zbMATH DE number 1953028 (Why is no real title available?)
• scientific article; zbMATH DE number 1979542 (Why is no real title available?)

This page was built for publication: Refining and compressing abstract model checking

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