Towards a formal treatment of implicit invocation using rely/guarantee reasoning

DOI10.1007/S001650050011zbMATH Open0934.68059OpenAlexW2046638690MaRDI QIDQ1293883FDOQ1293883

Authors: K. Appert 

Publication date: 29 June 1999

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s001650050011

Recommendations

• On rely-guarantee reasoning
• scientific article; zbMATH DE number 6774232
• scientific article; zbMATH DE number 1956564
• Explicit stabilisation for modular rely-guarantee reasoning
• The Rely-Guarantee method for verifying shared variable concurrent programs

zbMATH Keywords

implicit invocationlarge-scale system design

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Cited In (3)

• An algebraic semantics of event-based architectures
• Using source transformation to test and model check implicit-invocation systems
• A parametric rely-guarantee reasoning framework for concurrent reactive systems

This page was built for publication: Towards a formal treatment of implicit invocation using rely/guarantee reasoning

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