Sciweavers

Share
CADE
2008
Springer

Model Checking for Stability Analysis in Rely-Guarantee Proofs

9 years 3 months ago
Model Checking for Stability Analysis in Rely-Guarantee Proofs
Rely-guarantee (RG) reasoning is useful for modular Hoare-style proofs of concurrent programs. However, RG requires that assertions be proved stable under the actions of the environment. We cast stability analysis as a model checking problem and show how this may be of use in interactive and automatic verification.
Hasan Amjad, Richard Bornat
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2008
Where CADE
Authors Hasan Amjad, Richard Bornat
Comments (0)
books