scientific article; zbMATH DE number 4213463

MaRDI QIDQ3359774zbMATH OpenFDO

Authors Peter Grønning, Thomas Qvist Nielsen, Hans Henrik Loevengreen

Publication date 1990

zbMATH Keywords

compositional verificationrely-guarantee specificationsafety propertiesshared variablesspecification and verification of concurrent systems

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) 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

• Pattern-based refinement of assume-guarantee specifications in reactive synthesis
• A Structural Proof of the Soundness of Rely/guarantee Rules
• Transformations for compositional verification of assumption-commitment properties
• Compositional synthesis via a convex parameterization of assume-guarantee contracts
• A rely-guarantee-based simulation for verifying concurrent program transformations
• Generalised rely-guarantee concurrency: an algebraic foundation
• Automated Assume-Guarantee Reasoning by Abstraction Refinement

Cited in

(5)

• Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency
• Application of the composition principle to unity-like specifications
• Assumption/guarantee specifications in linear-time temporal logic (extended abstract)
• Assumption/guarantee specifications in linear-time temporal logic
• Specification of concurrent objects using auxiliary variables

This page was built for publication:

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