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
  • 24
    total views
  • 0
    total downloads
  • 3
    views this month
  • 0
    downloads this month

Export as

Related outputs

Describing and simulating concurrent quantum systems
Bornat, R., Boender, J., Kammueller, F., Poly, G. and Nagarajan, R. 2020. Describing and simulating concurrent quantum systems. Biere, A. and Parker, D. (ed.) International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 20). Dublin 27 - 30 Apr 2020 Springer. pp. 271-277 https://doi.org/10.1007/978-3-030-45237-7_16
New lace and arsenic: adventures in weak memory with a program logic (v2)
Bornat, R., Alglave, J. and Parkinson, M. 2016. New lace and arsenic: adventures in weak memory with a program logic (v2). arXiv.org arXiv. https://doi.org/10.48550/arXiv.1512.01416
Separation logic and concurrency
Bornat, R. 2010. Separation logic and concurrency. in: Boca, P., Bowen, J. and Siddiqi, J. (ed.) Formal Methods: State of the Art and New Directions London Springer Verlag. pp. 217-248
Inter-process buffers in separation logic with rely-guarantee
Bornat, R. and Amjad, H. 2010. Inter-process buffers in separation logic with rely-guarantee. Formal Aspects of Computing. 22 (6), pp. 735-772. https://doi.org/10.1007/s00165-009-0141-8
Explanation of two non-blocking shared-variable communication algorithms
Bornat, R. and Amjad, H. 2011. Explanation of two non-blocking shared-variable communication algorithms. Formal Aspects of Computing. https://doi.org/10.1007/s00165-011-0213-4
Variables as resource in Hoare logic.
Bornat, R., Calcagno, C. and Parkinson, M. 2006. Variables as resource in Hoare logic. in: 21st Annual IEEE Symposium on Logic in Computer Science (LICS 2006), Seattle, Washington. Proceedings. IEEE Computer Society. pp. 137-146
Variables as resources in separation logic.
Bornat, R., Calcagno, C. and Yang, H. 2006. Variables as resources in separation logic. 21st Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXI), Birmingham, UK. Proceedings in Electronic Notes in Theoretical Computer Science. Elsevier B.V.. 155, pp. 247-276. https://doi.org/10.1016/j.entcs.2005.11.059
Cyclic proofs of program termination in separation logic
Brotherston, J., Bornat, R. and Calcagno, C. 2008. Cyclic proofs of program termination in separation logic. ACM SIGPLAN Notices. 43 (1), pp. 101-112. https://doi.org/10.1145/1328897.1328453
Modular verification of a non-blocking stack.
Bornat, R., Parkinson, M. and O'Hearn, P. 2007. Modular verification of a non-blocking stack. 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '07), Nice, France. Proceedings.. https://doi.org/10.1145/1190216.1190261
Permission accounting in separation logic.
Bornat, R., Calcagno, C., Parkinson, M. and O'Hearn, P. 2005. Permission accounting in separation logic. 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '05), Long Beach, California, USA. Proceedings. https://doi.org/10.1145/1047659.1040327