Towards Automatic Stability Analysis for Rely-Guarantee Proofs

The Rely-Guarantee approach is a well-known compositional method for proving Hoare logic properties of concurrent programs. In this approach, predicates in the proof must be proved invariant (or stable) under interference from the environment. We describe a framework, and a prototype implementation, for automatically detecting and repairing instability in such proofs. The method uses a combination of model , abstract interpretation, SMT and flow-control refinement.

• Type: Conference
• Year: 2009
• Where: VMCAI
• Authors: Hasan Amjad, Richard Bornat
• Keywords: Hoare Logic Properties, Rely-Guarantee Approach, Software Engineering, VMCAI 2009, Well-known Compositional Method