This paper, presented at the 17th Annual IEEE Symposium on Logic in Computer Science, introduces an extension of Hoare logic called Separation Logic, developed by John C. Reynolds and others. This logic is designed to reason about low-level imperative programs that use shared mutable data structures. The key innovation is the introduction of a "separating conjunction" and a "separating implication," which allow for the precise description of structures with controlled sharing. The paper surveys the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. It also discusses future directions for research. The authors provide a detailed formalization of the programming language, the assertion language, and the inference rules for specifications, emphasizing the use of the frame rule for local reasoning about the heap. The paper includes examples of specifications and proofs, particularly for list and tree structures, to illustrate the effectiveness of Separation Logic in reasoning about complex programs.This paper, presented at the 17th Annual IEEE Symposium on Logic in Computer Science, introduces an extension of Hoare logic called Separation Logic, developed by John C. Reynolds and others. This logic is designed to reason about low-level imperative programs that use shared mutable data structures. The key innovation is the introduction of a "separating conjunction" and a "separating implication," which allow for the precise description of structures with controlled sharing. The paper surveys the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. It also discusses future directions for research. The authors provide a detailed formalization of the programming language, the assertion language, and the inference rules for specifications, emphasizing the use of the frame rule for local reasoning about the heap. The paper includes examples of specifications and proofs, particularly for list and tree structures, to illustrate the effectiveness of Separation Logic in reasoning about complex programs.