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

DOI10.1007/S001650050011MaRDI QIDQ1293883zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

implicit invocationlarge-scale system design

Mathematics Subject Classification ID

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

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

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)