Towards Automatic Stability Analysis for Rely-Guarantee Proofs

DOI10.1007/978-3-540-93900-9_6zbMATH Open1206.68084OpenAlexW1518902272MaRDI QIDQ3600463FDOQ3600463

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

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

Mathematics Subject Classification ID

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

Cited In (5)

• Title not available (Why is that?)
• Title not available (Why is that?)
• 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

Uses Software

• Apron
• BLAST
• cvc3
• Interproc

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)