Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

14

CADE
2008
Springer

favoriteEmaildiscussreport

141views Logical Reasoning» more CADE 2008»

Model Checking for Stability Analysis in Rely-Guarantee Proofs

14 years 4 months ago

Model Checking for Stability Analysis in Rely-Guarantee Proofs

Download sunsite.informatik.rwth-aachen.de

Rely-guarantee (RG) reasoning is useful for modular Hoare-style proofs of concurrent programs. However, RG requires that assertions be proved stable under the actions of the environment. We cast stability analysis as a model checking problem and show how this may be of use in interactive and automatic verification.

Hasan Amjad, Richard Bornat

Real-time Traffic

Automated Reasoning | CADE 2008 | Model Checking Problem | Modular Hoare-style Proofs |

claim paper

Related Content

» Towards Automatic Stability Analysis for RelyGuarantee Proofs

» Formal Analysis of a SelfStabilizing Algorithm Using Predicate Diagrams

» From Model Checking to a Temporal Proof

» Proof Slicing with Application to Model Checking Web Services

» Incremental Inductive CTL Model Checking

» AssertionBased Analysis of Hybrid Systems with PVS

» An Accurate Link Model and Its Application to Stability Analysis of FAST TCP

» Tests Proofs and Refinements

» Theoretical improvements in the stability analysis of a new class of modelfree visual serv...

Post Info
More Details (n/a)

Added	03 Dec 2009
Updated	03 Dec 2009
Type	Conference
Year	2008
Where	CADE
Authors	Hasan Amjad, Richard Bornat

Comments (0)