for Hoare triples where the preconditions and postconditions are formulae interpreted over an arbitrary partial commutative monoid instead of a particular heap model. Later, by suitable choice of commutative monoid, it was surprisingly found that the proof rules of abstract versions of concurrent separation logic could be used to reason about interfering concurrent processes, for example by encoding the rely-guarantee technique which had been originally proposed to reason about interference; in this work the elements of the model were considered not resources, but rather "views" of the program state, and a non-standard interpretation of Hoare triples accompanies the non-standard reading of pre and postconditions. Finally, CSL-style principles have been used to compose reasoning about program histories instead of program states, in order to provide modular techniques for reasoning about fine-grained concurrent algorithms. Versions of CSL have been included in many interactive and semi-automatic (or "in-between") verification tools as described in the next section. A particularly significant verification effort is that of the μC/OS-II kernel mentioned there. But, although steps have been made, as of yet CSL-style reasoning has been included in comparatively few tools in the automatic program analysis category (and none mentioned in the next section). O'Hearn and Brookes are co-recipients of the 2016 Gödel Prize for their invention of Concurrent Separation Logic. Verification and program analysis tools Tools for reasoning about programs fall on a spectrum from fully automatic program analysis tools, which do not require any user input, to interactive tools where the human is intimately involved in the proof process. Many such tools have been developed; the following list includes a few representatives in each category. Automatic Program Analyses. These tools typically look for restricted classes of bugs (e.g., memory safety errors) or attempt to prove their absence, but fall short of proving full correctness. A current example is Facebook Infer, a static analysis tool for Java, C, and Objective-C based on separation logic and bi-abduction. As of 2015 hundreds of bugs per month were being found by Infer and fixed by developers before being shipped to Facebook's mobile apps Other examples include SpaceInvader (one of the first SL analyzers), Predator (which has won several verification competitions), MemCAD (which mixes shape and numerical properties) and SLAyer (from Microsoft Research, focussed on data structures found in device drivers) Interactive Proof. Proofs have been done using embeddings of Separation Logic into interactive theorem provers such as the Coq