[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Proof-Outlines for Threads in Java

  • Conference paper
  • First Online:
CONCUR 2000 — Concurrency Theory (CONCUR 2000)

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

Included in the following conference series:

Abstract

We introduce an assertional method for specifying and proving properties of the multi-threaded flow of control in Java. The method integrates in a modular manner reasoning about the shared-variable concurrency within one object and the communication of values between threads.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 71.50
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 89.99
Price includes VAT (United Kingdom)
  • 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.

Similar content being viewed by others

References

  1. K. R. Apt: Ten years of Hoare logic: a survey — part I. ACM Transactions on Programming Languages and Systems, Vol. 3, No. 4, October 1981, pp. 431–483.

    Article  MATH  Google Scholar 

  2. K. R. Apt. Formal justification of a proof system for Communicating Sequential Processes. Journal of the ACM, Vol. 30, No. 1, January 1983, pp. 197–216.

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MATH  Google Scholar 

  4. E. Boerger and W. Schulte. Modular Design for the Java Virtual Machine Architecture. In Architecture Design and Validation Methods. Lecture Notes in Computer Science, 1999.

    Google Scholar 

  5. F. S. de Boer. A proof system for the parallel object-oriented language POOL. Proceedings of the seventeenth International Colloquium on Automata, Languages and Programming (ICALP), Lecture Notes in Computer Science, Vol. 443, 1990.

    Chapter  Google Scholar 

  6. P. Cenciarelli, A. Knapp, B. Reus, and M. Wirsing. An Event-Based Structural Operational Semantics of Multi-Threaded Java. In Formal Syntax and Semantics of Java, Lecture Notes in Computer Science, Vol. 1523, 1999.

    Chapter  Google Scholar 

  7. R. T. Gerth and W.-P. de Roever. Proving monitors revisited: A first step towards verifying object oriented systems. Fundamenta informaticae IX, North-Holland, p. 371–400, 1986.

    Google Scholar 

  8. U. Hensel, M. Huisman, B. Jacobs, and H. Tews. Reasoning about Classes in Object-Oriented Languages: Logical Models and Tools. Proceedings of the European Symposium on Programming, Lecture Notes in Computer Science, Vol. 1381, 1998.

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  10. J. V. Tucker and J. I. Zucker. Program Correctness over Abstract Data Types, with Error-State Semantics. CWI Monograph Series, Vol. 6, Centre for Mathematics and Computer Science/North-Holland, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Christian-Albrechts-University Kiel, Germany

    Erika Ábrahám-Mumm

  2. Utrecht University, The Netherlands

    Frank S. de Boer

Authors
  1. Erika Ábrahám-Mumm
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frank S. de Boer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Engineering, Pennsylvania State University, 220 Pond Laboratory, University Park, PA, 16802-6106, USA

    Catuscia Palamidessi

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ábrahám-Mumm, E., de Boer, F.S. (2000). Proof-Outlines for Threads in Java. In: Palamidessi, C. (eds) CONCUR 2000 — Concurrency Theory. CONCUR 2000. Lecture Notes in Computer Science, vol 1877. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44618-4_18

Download citation

  • DOI: https://doi.org/10.1007/3-540-44618-4_18

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67897-7

  • Online ISBN: 978-3-540-44618-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation