Separation logic

In computer science, separation logic[1] is an extension of Hoare logic, a way of reasoning about programs. It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang,[1][2][3][4] drawing upon early work by Rod Burstall.[5] The assertion language of separation logic is a special case of the logic of bunched implications (BI).[6] A CACM review article by O'Hearn charts developments in the subject to early 2019.[7]

  1. ^ a b Reynolds, John C. (2002). "Separation Logic: A Logic for Shared Mutable Data Structures" (PDF). LICS.
  2. ^ Reynolds, John C. (1999). "Intuitionistic Reasoning about Shared Mutable Data Structure". In Davies, Jim; Roscoe, Bill; Woodcock, Jim (eds.). Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford–Microsoft Symposium in Honour of Sir Tony Hoare. Palgrave.
  3. ^ Ishtiaq, Samin; O'Hearn, Peter (2001). "BI as an assertion language for mutable data structures". Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM. pp. 14–26. doi:10.1145/360204.375719. ISBN 1581133367. S2CID 2652274. {{cite book}}: |journal= ignored (help)
  4. ^ O'Hearn, Peter; Reynolds, John C.; Yang, Hongseok (2001). "Local Reasoning about Programs that Alter Data Structures". CSL. CiteSeerX 10.1.1.29.1331.
  5. ^ Burstall, R. M. (1972). "Some techniques for proving programs which alter data structures". Machine Intelligence. 7.
  6. ^ O'Hearn, P. W.; Pym, D. J. (June 1999). "The Logic of Bunched Implications". Bulletin of Symbolic Logic. 5 (2): 215–244. CiteSeerX 10.1.1.27.4742. doi:10.2307/421090. JSTOR 421090. S2CID 2948552.
  7. ^ O'Hearn, Peter (February 2019). "Separation Logic". Commun. ACM. 62 (2): 86–95. doi:10.1145/3211968. ISSN 0001-0782.