Sciweavers

ESOP
2010
Springer

Explicit Stabilisation for Modular Rely-Guarantee Reasoning

14 years 29 days ago
Explicit Stabilisation for Modular Rely-Guarantee Reasoning
Abstract. 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 RelyGuarantee, 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.
John Wickerson, Matthew J. Parkinson, Mike Dodds
Added 02 Mar 2010
Updated 02 Mar 2010
Type Conference
Year 2010
Where ESOP
Authors John Wickerson, Matthew J. Parkinson, Mike Dodds
Comments (0)