Towards Automatic Stability Analysis for Rely-Guarantee Proofs

摘要

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