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)

Full work available at URL https://doi.org/10.7561/SACS.2014.2.217

zbMATH Keywords

message-passingrely-guaranteetrace semantics

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55) 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

• 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)

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

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)