2005 | OriginalPaper | Buchkapitel
Abstraction Refinement for Bounded Model Checking
verfasst von : Anubhav Gupta, Ofer Strichman
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Counterexample-Guided Abstraction Refinement (
cegar
) techniques have been very successful in model checking large systems. While most previous work has focused on model checking, this paper presents a Counterexample-Guided abstraction refinement technique for Bounded Model Checking (
bmc
). Our technique makes
bmc
much faster, as indicated by our experiments.
bmc
is also used for generating refinements in the Proof-Based Refinement (
pbr
) framework. We show that our technique unifies
pbr
and
cegar
into an abstraction-refinement framework that can balance the model checking and refinement efforts.