Skip to main content
SpringerLink
Log in

A compositional proof system for shared variable concurrency

  • Conference paper
  • First Online:
FME '97: Industrial Applications and Strengthened Foundations of Formal Methods (FME 1997)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1313))

Included in the following conference series:

Abstract

This paper presents a compositional proof system for shared variable concurrency. The proof system is based on an assertion language which describes a computation, i.e. a sequence of state-changes, in terms of a qualitive notion of time represented by a discrete total well-founded ordering.

The research of F. S. de Boer has been partially supported by Human Capital and Mobility network EXPRESS.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K.R. Apt, N. Francez and W. P. de Roever. A proof system for Communicating Sequential Processes. In ACM Transactions on Programming Languages and Systems, 2:359–385, 1980.

    Article  Google Scholar 

  2. H. Barringer, R. Kuiper, and A. Pnueli. Now you may compose temporal logic specifications. In 16th ACM symposium on Theory of Computation, pages 51–63, 1984.

    Google Scholar 

  3. F.S. de Boer, J.N. Kok, C. Palamidessi, and J.J.M.M. Rutten. The failure of failures: Towards a paradigm for asynchronous communication. In Proceedings of Concur '91, Lecture Notes in Computer Science, Vol. 527, pages 111–126, 1991.

    Google Scholar 

  4. S. Brookes. A fully abstract semantics of a shared variable parallel language. In Proceedings 8th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, pages 98–109, 1993.

    Google Scholar 

  5. S.D. Brookes, C.A.R. Hoare and A.W. Roscoe. A Theory of Communicating Sequential Processes. JACM 31(7), pp. 560–599, 1984.

    MathSciNet  Google Scholar 

  6. S.A. Cook. Soundness and completeness of an axiom system for program verification. In SIAM J. on Computing 7, pp. 70–90, 1978.

    Article  Google Scholar 

  7. E.W. Dijkstra. Solution of a problem in concurrent programming control. In Comm. ACM 8, 1965.

    Google Scholar 

  8. E.W. Dijkstra. Co-operating sequential processes. In Academic Press, New York, 1968.

    Google Scholar 

  9. E.C.R. Hehner, C.A.R. Hoare. A more complete model of Communicating Processes. TCS 26, pp. 134–120, 1983.

    Google Scholar 

  10. J. Hooman. Specification and compositional verification of real-time systems. Lecture Notes in Computer Science, Vol. 558, 1992.

    Google Scholar 

  11. C.B. Jones. Development methods for computer programs including a notion of interference. PhD thesis, Oxford University Computing Laboratory, 1981.

    Google Scholar 

  12. M. Joseph, P. Pandya. Specification and Verification of Total Correctness of Distributed Programs. Research report RR 96, University of Warwick, 1987.

    Google Scholar 

  13. Y. Kesten, Z.Manna and A. Pnueli, Temporal verification of simulation and refinement. In A Decade of Concurrency (eds. J.W de Bakker, W.-P. de Roever and G. Rozenberg), Lecture Notes in Computer Science, Vol. 803, 1993.

    Google Scholar 

  14. L. Lamport. Verification and specification of concurrent programs. In A Decade of Concurrency (eds. J.W de Bakker, W.-P. de Roever and G. Rozenberg), Lecture Notes in Computer Science, Vol. 803, 1993.

    Google Scholar 

  15. J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Transactions on Software Engeneering, 7(7):417–426, 1981.

    Google Scholar 

  16. E.-R. Olderog and C.A.R. Hoare. Specification oriented Programming in TCSP. Proc. of the 10th ICALP, LNCS 154, 1983.

    Google Scholar 

  17. K. Stølen. Development of Parallel Programs on Shared Data-structures. PhD thesis, Computer Science Department, Manchester University, 1990.

    Google Scholar 

  18. N. Sounderarajan. Axiomatic semantics of communicating sequential processes. TOPLAS, 6:647–662, 1984.

    Google Scholar 

  19. J. Widom, D. Gries and F.B. Schneider. Completeness and Incompleteness of Trace-based Network Proof Systems. Proc. of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 27–38, 1987.

    Google Scholar 

  20. J.V. Tucker and J.I. Zucker. Program correctness over abstract data types, with error-state semantics. In CWI Monograph Series, vol. 6, Centre for Mathematics and Computer Science/North-Holland, 1988.

    Google Scholar 

  21. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. In Acta Informatika, 6:319–340, 1976.

    Google Scholar 

  22. Q. Xu. A theory of state-based parallel programming. PhD thesis, Oxford University Computing Laboratory, 1992.

    Google Scholar 

  23. Q. Xu, W.-P. de Roever and J. He. Rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing 1997 (To appear.

    Google Scholar 

  24. C.C. Zhou and C.A.R. Hoare. Partial Correctness of CSP. Proc. IEEE Int. Conf. on Distributed Computer Systems, pp. 1–12, 1981.

    Google Scholar 

  25. J. Zwiers. Compositionality, Concurrency, and Partial Correctness. Lecture Notes in Computer Science, Vol.321, Springer-Verlag, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Utrecht University, P.O. Box 80.089, 3508 TB, Utrecht, The Netherlands

    F. S. de Boer

  2. Institut für Informatik and Praktische Mathematik II, Christian- Albrechts-Universität zu Kiel, Preusserstrasse 1–9, 24105, Kiel, Germany

    U. Hannemann & W. -P. de Roever

Authors
  1. F. S. de Boer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. U. Hannemann
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. W. -P. de Roever
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

John Fitzgerald Cliff B. Jones Peter Lucas

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

de Boer, F.S., Hannemann, U., de Roever, W.P. (1997). A compositional proof system for shared variable concurrency. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds) FME '97: Industrial Applications and Strengthened Foundations of Formal Methods. FME 1997. Lecture Notes in Computer Science, vol 1313. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63533-5_27

Download citation

  • DOI: https://doi.org/10.1007/3-540-63533-5_27

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63533-8

  • Online ISBN: 978-3-540-69593-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation