We propose a new formalisation of stability for Rely-Guarantee, in which an assertion's stability is encoded into its syntactic form. This allows two advances in modular reasoning. Firstly, it enables Rely-Guarantee, for the first time, to verify concurrent libraries independently of their clients' environments. Secondly, in a sequential setting, it allows a module's internal interference to be hidden while verifying its clients. We demonstrate our approach by verifying, using RGSep, the Version 7 Unix memory manager, uncovering a twenty-year-old bug in the process. � 2010 Springer-Verlag.
CITATION STYLE
Wickerson, J., Dodds, M., & Parkinson, M. (2010). Explicit Stabilisation for Modular Rely-Guarantee Reasoning (pp. 610–629). https://doi.org/10.1007/978-3-642-11957-6_32
Mendeley helps you to discover research relevant for your work.