Concrete model checking with abstract matching and refinement

DOI10.1007/11513988_7MaRDI QIDQ5716598zbMATH OpenOpenAlexFDO

Authors Radek Pelánek, Willem Visser, Corina S. Păsăreanu

Publication date 10 January 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b138445

Mathematics Subject Classification ID

Theory of software (68N99) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Abstraction and Refinement in Model Checking
• The abstraction-refinement framework in model checking
• An efficient approach for abstraction-refinement in model checking
• Model Checking Software
• Model checking with formula-dependent abstract models
• Refining and compressing abstract model checking
• Abstraction refinement for bounded model checking
• Model checking and abstraction
• An algebraic framework for abstract model checking
• A satisfiability-based approach to abstraction refinement in model checking

Cited in

(12)

• Efficient bounded model checking of heap-manipulating programs using tight field bounds
• Finding feasible counter-examples when model checking abstracted Java programs
• Approximating Behaviors in Embedded System Design
• Software model checking with abstraction refinement
• Lazy abstraction
• Efficient property preservation checking of model refinements
• Symbolic Execution Techniques for Refinement Testing
• Model Checking Software
• Concrete abstractions. Formalizing and analyzing discrete theories and algorithms with the RISCAL model checker
• The reachable simulation problem
• Computing reachable simulations on transition systems
• 3-valued abstraction: More precision at less cost

Describes a project that uses

Uses Software

• Rostra
• veriSoft

This page was built for publication: Concrete model checking with abstract matching and refinement

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