Rely-guarantee references for refinement types over aliased mutable data.

Colin S. Gordon, Michael D. Ernst, Dan Grossman

Browse the full PLDI paper archive.