RT DW A1 He, Paul. T1 Rely-Guarantee Semantics for Separation-Logic-Based Specification Extraction