Rely-guarantee based reasoning for message-passing programs

DOI10.7561/SACS.2014.2.217MaRDI QIDQ4621182zbMATH OpenFDO

Authors Jinjiang Lei, Zongyan Qiu

Publication date 8 February 2019

Published in Scientific Annals of Computer Science (Search for Journal in Brave)

zbMATH Keywords

message-passingrely-guaranteetrace semantics

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Modular reasoning for message-passing programs
• Local rely-guarantee reasoning
• Taming Message-Passing Communication in Compositional Reasoning About Confidentiality
• scientific article; zbMATH DE number 6774232
• Permission-based separation logic for message-passing concurrency

Cited in

(6)

• Modular reasoning for message-passing programs
• scientific article; zbMATH DE number 6774232 (Why is no real title available?)
• Computing race variants in message-passing concurrent programming with selective receives
• Taming Message-Passing Communication in Compositional Reasoning About Confidentiality
• Practical abstractions for automated verification of message passing concurrency
• Local rely-guarantee reasoning

This page was built for publication: Rely-guarantee based reasoning for message-passing programs

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