Outline of this talk 。Background Concurrent Separation Logic -Assume-Guarantee reasoning SAGL:combination of CSL A-G reasoning Interpretation of CSL in SAGLOutline of this talk • Background – Concurrent Separation Logic – Assume-Guarantee reasoning • SAGL: combination of CSL & A-G reasoning • Interpretation of CSL in SAGL