Abstract
We give complete mathematial foundations for the method, recently
developed by Chou, Mannava, and Park, for verifying safety
properties of cache coherence protocols. The method employs a
specific form of counterexample-guided abstraction refinement and is
originally described on worked-out examples of the German and FLASH
protocols. We describe and prove the method at an abstract level,
thus establishing its scope and opening the way to its further
mechanization.
Users
Please
log in to take part in the discussion (add own reviews or comments).