Towards automatic stability analysis for rely-guarantee proofs

Book chapter

Amjad, H. and Bornat, R. 2009. Towards automatic stability analysis for rely-guarantee proofs. in: Jones, N. and Müller-Olm, M. (ed.) Verification, model checking, and abstract interpretation: 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings Springer.
Chapter titleTowards automatic stability analysis for rely-guarantee proofs
AuthorsAmjad, H. and Bornat, R.
Abstract

The Rely-Guarantee approach is a well-known compositional method for proving Hoare logic properties of concurrent programs. In this approach, predicates in the proof must be proved invariant (or stable) under interference from the environment. We describe a framework, and a prototype implementation, for automatically detecting and repairing instability in such proofs. The method uses a combination of model checking, abstract interpretation, SMT and flow-control refinement.

Research GroupFoundations of Computing group
Book titleVerification, model checking, and abstract interpretation: 10th International Conference, VMCAI 2009, Savannah, GA, USA, January 18-20, 2009. Proceedings
EditorsJones, N. and Müller-Olm, M.
PublisherSpringer
SeriesLecture Notes in Computer Science
ISBN
Hardcover9783540938996
ISSN0302-9743
Publication dates
Print2009
Publication process dates
Deposited22 Nov 2013
Output statusPublished
Additional information

Series ISSN: 0302-9743. Online ISBN: 9783540939009

Digital Object Identifier (DOI)https://doi.org/10.1007/978-3-540-93900-9_6
LanguageEnglish
Permalink -

https://repository.mdx.ac.uk/item/8490x

Log in to edit
  • 12
    total views
  • 0
    total downloads
  • 0
    views this month
  • 0
    downloads this month

Export as