Skip to main content
SpringerLink
Log in

Towards Automatic Stability Analysis for Rely-Guarantee Proofs

  • Conference paper
Verification, Model Checking, and Abstract Interpretation (VMCAI 2009)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5403))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Lamport, L.: Conjoining specifications. Technical Report 118, DEC Systems Research Center (1993)

    Google Scholar 

  2. Alur, R., de Alfaro, L., Henzinger, T.A., Mang, F.Y.C.: Automating modular verification. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 82–97. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  3. APRON project, http://apron.cri.ensmp.fr/

  4. Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker BLAST. STTT 9(5-6), 505–525 (2007)

    Article  Google Scholar 

  6. Calcagno, C., Parkinson, M.J., Vafeiadis, V.: Modular safety checking for fine-grained concurrency. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 233–248. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  7. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. The MIT Press, Cambridge (1999)

    Google Scholar 

  8. Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  9. Distefano, D., O’Hearn, P., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Dodds, M., Feng, X., Parkinson, M., Vafeiadis, V.: Deny-guarantee reasoning (2008) (Draft)

    Google Scholar 

  11. Flanagan, C., Freund, S.N., Qadeer, S., Seshia, S.A.: Modular verification of multithreaded programs. Theor. Comput. Sci. 338(1-3), 153–183 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  12. Gotsman, A., Cook, B., Parkinson, M., Vafeiadis, V.: Proving liveness properties of non-blocking data structures. In: POPL (submitted, 2008)

    Google Scholar 

  13. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  14. Hoare, C.A.R.: An axiomatic basis for programming. Communications of the ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  15. Interproc static analyzer, http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/index.html

  16. Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)

    Google Scholar 

  17. Michael, M.M., Scott, M.L.: Simple, fast, and practical non-blocking and blocking concurrent queue algorithms. In: PODC 1996: Proceedings of the fifteenth annual ACM symposium on Principles of distributed computing, pp. 267–275. ACM Press, New York (1996)

    Chapter  Google Scholar 

  18. Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun. ACM 19(5), 279–285 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  19. Saïdi, H.: Model checking guided abstraction and analysis. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 377–396. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  20. Simpson, H.R.: Four-Slot Fully Asynchronous Communication Mechanism. IEE Proceedings 137(1), 17–30 (1990)

    Google Scholar 

  21. Viktor Vafeiadis. Modular fine-grained concurrency verification. PhD thesis, University of Cambridge (2007)

    Google Scholar 

  22. Vafeiadis, V., Parkinson, M.J.: A Marriage of Rely/Guarantee and Separation Logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 256–271. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Middlesex University School of Computing Science, London, NW4 4BT, UK

    Hasan Amjad & Richard Bornat

Authors
  1. Hasan Amjad
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Richard Bornat
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. (Emeritus University of Copenhagen), Bukkeballevej 88, 2960, Rungsted, Denmark

    Neil D. Jones

  2. Institut für Informatik, Fachbereich Mathematik und Informatik, Westfälische Wilhelms-Universität, 48149, Münster, Germany

    Markus Müller-Olm

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Amjad, H., Bornat, R. (2008). Towards Automatic Stability Analysis for Rely-Guarantee Proofs. In: Jones, N.D., Müller-Olm, M. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2009. Lecture Notes in Computer Science, vol 5403. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-93900-9_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-93900-9_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-93899-6

  • Online ISBN: 978-3-540-93900-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation