Technology · Verification & Validation
Abstraction
Replacing part of a design with a simpler over-approximation, such as cutting a counter, blackboxing a memory or reducing a data width, so that a formal proof becomes tractable.
Sound abstractions may produce spurious counterexamples but never miss real bugs.
- Also known as
- Counter abstraction, Blackboxing
- Type
- Technology
- Domain
- Verification & Validation, Formal verification
Notes
CEGAR, counterexample-guided abstraction refinement, automates the loop of abstracting and re-refining.
Related terms
- State space explosion
- Model checking
- Bounded proof
- COI
Part of the Verification & Validation glossary, with every term in the topic and the lifecycles, tools and standards that use them.
Where it appears on the Hub
No other page of the Hub uses this term yet.
Suggest an improvement
Suggest an improvement to this entry
A clearer definition, an example, a correction or a source an editor can check. Editors review every suggestion before the entry changes.
Last reviewed: not yet reviewed in depth. Entry last updated . The full glossary