Sciweavers

LICS
2002
IEEE

Separation Logic: A Logic for Shared Mutable Data Structures

13 years 8 months ago
Separation Logic: A Logic for Shared Mutable Data Structures
In joint work with Peter O’Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure. The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a “separating conjunction” that asserts that its subformulas hold for disjoint parts of the heap, and a closely related “separating implication”. Coupled with the induc
John C. Reynolds
Added 15 Jul 2010
Updated 15 Jul 2010
Type Conference
Year 2002
Where LICS
Authors John C. Reynolds
Comments (0)