Since the pioneering works of Floyd and Hoare, a great deal of formal methods have been proposed to guarantee different program properties. Due to undecidability, most analysis techniques introduce some kind of approximation to make the problem tractable. This can be over-approximation, to guarantee program correctness, or under-approximation, to find bugs. In the talk, we will classify some known program logics depending on their approximation and discuss relations between them, leading to some observations on the intrinsic differences between over and under-approximation. Then, we will talk about a new logic for backward under-approximation, a condition which was already known in the literature but that missed a dedicated program logic. We present Sufficient Incorrectness Logic (SIL), a sound and complete proof system, and instantiate the same idea in Separation SIL, a proof system based on Separation Logic to handle dynamic heap management.