The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Refinement strategies for verification methods based on datapath abstraction
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
In this paper we explore the application of Counter example-Guided Abstraction Refinement (CEGAR) in the context of microprocessor correspondence checking. The approach utilizes automatic datapath abstraction, augmented with automatic refinement based on 1) localization, 2) generalization, and 3) minimal unsatisfiable subset (MUS) extraction. We introduce several refinement strategies and empirically evaluate their effectiveness on a set of microprocessor benchmarks. The data suggest that localization, generalization, and MUS extraction from both the abstract and concrete models are essential for effective verification. Additionally, refinement tends to converge faster when multiple MUses are extracted in each iteration.
How it got here
How it got here
agent via openalex
Added
2026-10-26 02:33 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@misc{andraus2006refinement,
title = {Refinement strategies for verification methods based on datapath abstraction},
author = {Zaher S. Andraus and Mark H. Liffiton and Karem A. Sakallah},
year = {2006},
journal = {Asia and South Pacific Design Automation Conference (ASP-DAC)},
pages = {19},
doi = {10.1145/1118299.1118306},
}