Separation Logic

Communications of the ACM (CACM)

Abstract

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.

Latest Publications

Sustainable AI: Environmental Implications, Challenges and Opportunities

Carole-Jean Wu, Ramya Raghavendra, Udit Gupta, Bilge Acun, Newsha Ardalani, Kiwan Maeng, Gloria Chang, Fiona Aga Behram, James Huang, Charles Bai, Michael Gschwind, Anurag Gupta, Myle Ott, Anastasia Melnikov, Salvatore Candido, David Brooks, Geeta Chauhan, Benjamin Lee, Hsien-Hsin S. Lee, Bugra Akyildiz, Max Balandat, Joe Spisak, Ravi Jain, Mike Rabbat, Kim Hazelwood

MLSys - 2022