Cover Image
QR Code

Separation Logic.

The article examines the use of separation logic in reasoning about computer programs. It looks at how separation logic supports scalable reasoning through the frame rule, an inference rule that allows a proof to be localized to the resources that a program component accesses. Concurrent separation...

Full description

Published in:Communications of the ACM Vol. 62; no. 2; pp. 86 - 96
Main Author: O’HEARN, PETER
Format: Article
Published: Association for Computing Machinery Feb2019
Subjects:
Computer programming
Logic
Reasoning
Frame relay (Data transmission)
Online Access:View this record in EBSCOhost
Summary:The article examines the use of separation logic in reasoning about computer programs. It looks at how separation logic supports scalable reasoning through the frame rule, an inference rule that allows a proof to be localized to the resources that a program component accesses. Concurrent separation logic is also covered.