Verification method based on decomposition of states in rely-guarantee/sep logic

We propose new method in this paper for local RGSep reasoning. Our method support a hiding rule for hiding the local sharing of resources from the outside world. These rules allow us to write local rely/guarantee conditions and improve the reusability of veryfied program modules.