%0 Journal Article %1 xx %A Krstic, Sava %D 2005 %E ?, %K abstraction cmp parameterized refinement verification %T Parametrized System Verification with Guard Strengthening and Parameter Abstraction %U http://www.csee.ogi.edu/~krstics/psfiles/ParamSys.pdf %X 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.

@article{xx, 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. }, added-at = {2010-05-04T09:32:42.000+0200}, author = {Krstic, Sava}, biburl = {https://www.bibsonomy.org/bibtex/267226c680c30567aed7c4259a251f414/giuliano.losa}, description = {Parametrized System Verification with Guard Strengthening and Parameter Abstraction}, editor = {?}, interhash = {f0bc0edf8b897fbb5bd9596d63559f85}, intrahash = {67226c680c30567aed7c4259a251f414}, keywords = {abstraction cmp parameterized refinement verification}, timestamp = {2010-05-04T09:32:42.000+0200}, title = {Parametrized System Verification with Guard Strengthening and Parameter Abstraction}, url = {http://www.csee.ogi.edu/~krstics/psfiles/ParamSys.pdf}, year = 2005 }