Friends Need a Bit More: Maintaining Invariants Over Shared State", editor = Dexter Kozen and Carron Shankland, booktitle = Mathematics of Program Construction, 7th International Conference, MPC 2004, Stirling, Scotland, UK, July 12-14, 2004, Proceedings,