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

Federated Learning for User Privacy and Data Confidentiality Workshop At ICML - July 24, 2021

Federated Learning with Buffered Asynchronous Aggregation

John Nguyen, Kshitiz Malik, Hongyuan Zhan, Ashkan Yousefpour, Michael Rabbat, Mani Malek, Dzmitry Huba

TSE - June 29, 2021

Learning From Mistakes: Machine Learning Enhanced Human Expert Effort Estimates

Federica Sarro, Rebecca Moussa, Alessio Petrozziello, Mark Harman

IEEE ICIP - September 19, 2021

Rate Estimation Techniques for Encoder Parallelization

Gaurang Chaudhari, Hsiao-Chiang Chuang, Igor Koba, Hariharan Lalgudi

RecSys - September 27, 2021

Jointly Optimize Capacity, Latency and Engagement in Large-scale Recommendation Systems

Hitesh Khandelwal, Viet Ha-Thuc, Avishek Dutta, Yining Lu, Nan Du, Zhihao Li, Qi Huang

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