Towards Automatic Stability Analysis for Rely-Guarantee Proofs

DOI10.1007/978-3-540-93900-9_6MaRDI QIDQ3600463zbMATH OpenOpenAlexFDO

Authors Hasan Amjad, Richard Bornat

Publication date 10 February 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-93900-9_6

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Explicit stabilisation for modular rely-guarantee reasoning
• A Structural Proof of the Soundness of Rely/guarantee Rules
• scientific article; zbMATH DE number 3938541
• Automated Assume-Guarantee Reasoning by Abstraction Refinement
• Towards Automatic Convergence Verification of Self-stabilizing Algorithms
• Assume-guarantee verification for probabilistic systems
• scientific article; zbMATH DE number 1696676
• Formal Reliability Analysis Using Theorem Proving

Cited in

(5)

• scientific article; zbMATH DE number 1956564 (Why is no real title available?)
• scientific article; zbMATH DE number 3938541 (Why is no real title available?)
• A Structural Proof of the Soundness of Rely/guarantee Rules
• Inter-process buffers in separation logic with rely-guarantee
• Explicit stabilisation for modular rely-guarantee reasoning

Describes a project that uses

Uses Software

• Interproc
• cvc3
• BLAST
• Apron

This page was built for publication: Towards Automatic Stability Analysis for Rely-Guarantee Proofs

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