In computing practice methods for showing the presence of bugs are pervasive and have major impact. But scientific research in program logic and (static) program analysis has overwhelmingly concentrated on meth- ods for proving the absence of bugs rather than their presence. Incor- rectness Logic (IL) has recently been advanced by O’Hearn as a logical under-approximate theory for proving the presence of bug compositionally – the flipside of Hoare Logic, which is an over-approximate compositional theory for proving the absence of bugs. To facilitate scalable bug detec- tion, Raad, O’Hearn and others later developed incorrectness separation logic (ISL) by marrying the under-approximate reasoning of IL with the local reasoning of separation logic and its frame rule. This locality leads to techniques that are compositional both in code (concentrating on a pro- gram component) and in the resources accessed (spatial locality), without tracking the entire global state or the global program within which a com- ponent sits. This enables reasoning to scale to large teams and codebases: reasoning can be done even when a global program is not present. Le, O’Hearn, Raad and others then developed Pulse-X, an automatic program analysis for catching memory safety errors, underpinned by ISL. Pulse-X found a number of real bugs in codebases such as OpenSSL, which were subsequently confirmed and fixed. They have compared the performance of Pulse-X against the state-of-the-art tool Infer on a number of large programs; these comparisons show that Pulse-X is comparable with Infer in terms of performance, and in certain cases its fix-rate surpasses that of Infer.