A parametric rely-guarantee reasoning framework for concurrent reactive systems

DOI10.1007/978-3-030-30942-8_11MaRDI QIDQ6535947zbMATH OpenFDO

Authors Yongwang Zhao, David Sanán, Fuyuan Zhang, Yang Liu

Publication date 14 March 2024

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 1956564
• On rely-guarantee reasoning
• scientific article; zbMATH DE number 3938541
• Generalised rely-guarantee concurrency: an algebraic foundation
• Rely-guarantee reasoning for causally consistent shared memory

Cites work

• scientific article; zbMATH DE number 3930354 (Why is no real title available?)
• scientific article; zbMATH DE number 1956480 (Why is no real title available?)
• scientific article; zbMATH DE number 1956564 (Why is no real title available?)
• A rely-guarantee-based simulation for verifying concurrent program transformations
• An algebra of synchronous atomic steps
• CSimpl: a rely-guarantee-based framework for verifying concurrent programs
• Generalised rely-guarantee concurrency: an algebraic foundation
• Noninterference for operating system kernels
• On rely-guarantee reasoning
• Reactive Systems
• Refinement, decomposition, and instantiation of discrete models: application to Event-B
• Superposition refinement of reactive systems
• Tentative steps toward a development method for interfering programs
• The Rely-Guarantee method for verifying shared variable concurrent programs
• Towards a formal treatment of implicit invocation using rely/guarantee reasoning

This page was built for publication: A parametric rely-guarantee reasoning framework for concurrent reactive systems

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