This paper introduces the verification theory of separation logic, characteristics of separation logic, and some successful applications of separation logic. Researches on separation logic to support program verification are analyzed, including the properties of separation logic, its relation to other logics, its support to programming languages and design patterns, and the theorem provers’ support to separation logic. The problems encountered when separation logic is applied more widely are pointed out, and the future research directions are discussed.