Once upon a time, program logics, such as Hoare's logic, were solely the domain of theorists, used to construct manual proofs of tiny, intricate algorithms. In recent years the area has been reinvigorated by developments in both theory and practice. One such development is Separation Logic -- a member of an "exotic" branch of mathematical logic known as substructural logic -- which has provided a way of attacking the old problem of efficient reasoning about dynamically allocated objects in memory. In this talk I describe how you can go from this seemingly exotic logic to a practical software tool for verifying selected integrity properties of low-level systems programs.

Along the way, I will draw in some concepts from artificial intelligence and the philosophy of science that help to significantly boost the level of automation in the tool.

Peter O'Hearn is a Professor of Computer Science at Queen Mary, University of London. O'Hearn's research is in the logic and semantics of computation. Throughout the 1990s, he worked on denotational semantics of programs. Then, around the turn of the millennium, he and John Reynolds discovered Separation Logic, which addressed the 30 year-old problem of efficient reasoning about linked data structures in memory. He went on to develop a Concurrent Separation Logic, which provides a modular proof method for shared-memory concurrent programs. Recently, with a vibrant community of researchers in the southeast of England, he has been tackling the problem of automatic verification and analysis of programs' use of the heap, as well as automatic program-termination analysis. This particularly involves the SpaceInvader team (Cristiano Calcagno, Dino Distefano, Hongseok Yang and O'Hearn) in London and their SLAyer/TERMINATOR colleagues at Microsoft Cambridge (Josh Berdine, Byron Cook). In 2007 O'Hearn received the Royal Society Wolfson Research Merit Award for his work on semantics, logic, and program analysis.