Graphical models of separation logic
Graphs are used to model control and data flow among events occurring in the execution of a concurrent program. Our treatment of data flow covers both shared storage and external communication. Nevertheless, the laws of Hoare and Jones correctness reasoning remain valid when interpreted in this general model. (C) 2009 Elsevier B.V. All rights reserved.
concurrency formal semantics