Reasoning about separation using abstraction and reification

DOI10.1007/978-3-319-22969-0_1MaRDI QIDQ5268439zbMATH OpenOpenAlexFDO

Authors Nisansala Yatapanage, Cliff B. Jones

Publication date 20 June 2017

Published in Software Engineering and Formal Methods (Search for Journal in Brave)

Full work available at URL https://eprint.ncl.ac.uk/fulltext.aspx?url=213823/8231E0BB-14FC-46C2-9034-E59A94F53B96.pdf&pub_id=213823

zbMATH Keywords

abstractionconcurrencyseparationownership

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• Separation logic and abstraction
• Separation logic and concurrency
• Modular reasoning about separation of concurrent data structures
• Fictional separation logic
• Syntactic control of interference for separation logic

Cites work

• scientific article; zbMATH DE number 1612488 (Why is no real title available?)
• scientific article; zbMATH DE number 46957 (Why is no real title available?)
• scientific article; zbMATH DE number 3584897 (Why is no real title available?)
• scientific article; zbMATH DE number 2090840 (Why is no real title available?)
• A Marriage of Rely/Guarantee and Separation Logic
• A logic covering undefinedness in program proofs
• An axiomatic basis for computer programming
• Balancing expressiveness in formal approaches to concurrency
• Modular Safety Checking for Fine-Grained Concurrency
• Reasoning about separation using abstraction and reification
• Resources, concurrency, and local reasoning
• Splitting atoms safely
• Tentative steps toward a development method for interfering programs
• The dynamic frames theory

Cited in

(5)

• Reasoning about separation using abstraction and reification
• Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example
• Possible values: exploring a concept for concurrency
• Separation logic and abstraction
• Specifying and reasoning about shared-variable concurrency

This page was built for publication: Reasoning about separation using abstraction and reification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5268439)