Research

In joint work with John Reynolds and others we developed Separation Logic as a formalism for reasoning about programs that mutate data structures. From a special logic for heaps it gradually evolved into a general theory for modular reasoning about concurrent as well as sequential programs. Separation Logic represents one of the most significant developments in the area of formal reasoning about programs since the founding works of Floyd and Hoare in the 1960s, opening up new lines of attack on longstanding open problems. Initially, it was shown how the “separating conjunction” connective short-circuits the effects of aliasing during reasoning, and this addressed the fundamental problem of efficient formal reasoning in the presence of pointer manipulation. Concurrent Separation Logic made inroads into a further open problem, that of modular reasoning about shared-memory concurrent programs. After the initial theoretical work an extended effort established that the logic provides a basis for efficient proof search in automatic and semiautomatic proof tools, for example giving rise to the Infer static analyzer, a tool that is in deployment at Facebook where it catches thousands of bugs per months before the code reaches production in products used by over a billion people daily.