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.

• Type: Conference
• Year: 2008
• Where: CADE
• Authors: Hasan Amjad, Richard Bornat
• Keywords: Automated Reasoning, CADE 2008, Model Checking Problem, Modular Hoare-style Proofs