Separation Logic

Communications of the ACM (CACM)


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.

Related Publications

All Publications

ISAAC - December 5, 2021

On the Extended TSP Problem

Julián Mestre, Sergey Pupyrev, Seeun William Umboh

ICML - July 24, 2021

Ditto: Fair and Robust Federated Learning Through Personalization

Tian Li, Shengyuan Hu, Ahmad Beirami, Virginia Smith

International Workshop on Realizing Artificial Intelligence Synergies in Software Engineering (RAISE) - September 26, 2021

Behavioural and Structural Imitation Models in Facebook’s WW Simulation System

John Ahlgren, Kinga Bojarczuk, Inna Dvortsova, Mark Harman, Rayan Hatout, Maria Lomeli, Erik Meijer, Silvia Sapora

ESEM - September 23, 2021

Measurement Challenges for Cyber Cyber Digital Twins: Experiences from the Deployment of Facebook’s WW Simulation System

Kinga Bojarczuk, Inna Dvortsova, Johann George, Natalija Gucevska, Mark Harman, Maria Lomeli, Simon Mark Lucas, Erik Meijer, Rubmary Rojas, Silvia Sapora

To help personalize content, tailor and measure ads, and provide a safer experience, we use cookies. By clicking or navigating the site, you agree to allow our collection of information on and off Facebook through cookies. Learn more, including about available controls: Cookies Policy