Specification and Verification of imperative programs that manipulate mutable data structures has always been a challenging problem. The main difficulty resides in the fact that when reasoning about such programs a global account of the heap has to be considered. Reynolds, O’Hearn and Yang have proposed an extension of Hoare Logic, Separation Logic, that enables local, compositional reasoning by allowing to focus only in the instructions “footprint”, i.e., the portion of the heap the instructions accesses. In this talk I will try to illustrate the key ideas behind Separation Logic informally and discuss some of its limitations. Also, I will briefly comment on the related ongoing work we are doing with César Sánchez and Gilles Barthe.