Modular reasoning for message-passing programs

DOI10.1007/978-3-319-10882-7_17MaRDI QIDQ2938169zbMATH OpenOpenAlexFDO

Authors Jinjiang Lei, Zongyan Qiu

Publication date 13 January 2015

Published in Theoretical Aspects of Computing – ICTAC 2014 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-10882-7_17

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Rely-guarantee based reasoning for message-passing programs
• Verifying the correctness of distributed systems via mergeable parallelism
• Modular verification for shared-variable concurrent programs
• Taming Message-Passing Communication in Compositional Reasoning About Confidentiality
• Permission-based separation logic for message-passing concurrency

Cited in

(9)

• Verifying the correctness of distributed systems via mergeable parallelism
• On verification of parallel message-passing processes
• A modular framework for verifying versatile distributed systems
• Computing race variants in message-passing concurrent programming with selective receives
• Rely-guarantee based reasoning for message-passing programs
• Taming Message-Passing Communication in Compositional Reasoning About Confidentiality
• Semantics of communication in simple multimodular programs
• Practical abstractions for automated verification of message passing concurrency
• Aneris: a mechanised logic for modular reasoning about distributed systems

This page was built for publication: Modular reasoning for message-passing programs

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