Skip to main content
SpringerLink
Log in

Introduction

  • Chapter
Verification of Sequential and Concurrent Programs

Part of the book series: Texts and Monographs in Computer Science ((MCS))

  • 82 Accesses

Abstract

This book is about program verification, with a special emphasis on verification of concurrent programs. Concurrent programs are usually difficult to design, and errors are more a rule than an exception. Consider, for example, the following simple problem.

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 74.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever

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. M. Aspnäs, R.J.R. Back, and K. Sere. The Hathi project: a project on parallel programming technology. Technical Report Ser. A, No 95, Departments of Computer Science and Mathematics, Abo Akademi, Finland, 1989.

    Google Scholar 

  2. 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 (3): 359–385, 1980.

    Article  MATH  Google Scholar 

  3. E. Ashcroft and Z. Manna Formalization of properties of parallel programs Machine Intelligence, 6: 17–41, 1971.

    MathSciNet  MATH  Google Scholar 

  4. K.R. Apt and E.-R. Olderog. Proof rules and transformations dealing with fairness. Science of Computer Programming, 3: 65100, 1983.

    Article  MathSciNet  Google Scholar 

  5. K.R. Apt. Correctness proofs of distributed termination algorithms. ACM Transactions on Programming Languages and Systems, 8: 388–405, 1986.

    Article  MATH  Google Scholar 

  6. R.C. Backhouse. Program Construction and Verification. Prentice-Hall International, Englewood Cliffs, NJ, 1986.

    Google Scholar 

  7. Bac89] R.J.R. Back. A method for refining atomicity in parallel algorithms. In PARLE Conference on Parallel Architectures and Languages Europe,pages 199–216, New York, 1989. Lecture Notes in Computer Science 366, Springer-Verlag.

    Google Scholar 

  8. J.A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information and Control, 60: 109–137, 1984.

    Article  MathSciNet  MATH  Google Scholar 

  9. J.A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37: 77121, 1985.

    Article  MathSciNet  Google Scholar 

  10. J.A. Bergstra and J.W. Klop. Algebra of communicating processes. In J.W. de Bakker, M. Hazewinkel, and J.K. Lenstra, editors, Proceedings CWI Symposium on Mathematics and Computer Science, pages 89–138, Amsterdam, 1986. North-Holland.

    Google Scholar 

  11. K.M. Chandy and J. Misra. Parallel Program Design: A Foundation. Addison-Wesley, New York, 1988.

    MATH  Google Scholar 

  12. CPS90] R. Cleaveland, J.G. Parrow, and B. Steffen. The concurrency workbench. In J. Sifakis, editor, Proceedings Workshop on Automatic Verification Methods for Finite State Systems,pages 2437, New York, 1990. Lecture Notes in Computer Science 407, Springer-Verlag.

    Google Scholar 

  13. E.W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs Communications of the ACM, 18: 453457, 1975.

    MathSciNet  Google Scholar 

  14. E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, N.J., 1976.

    MATH  Google Scholar 

  15. E.A. Emerson and E.M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2 (3): 241–266, 1982.

    Article  MATH  Google Scholar 

  16. R. Floyd. Assigning meaning to programs. In J.T. Schwartz, editor, Proceedings of Symposium on Applied Mathematics 19, Mathematical Aspects of Computer Science, pages 19–32, American Mathematical Society, New York, 1967.

    Google Scholar 

  17. L. Flon and N. Suzuki. The total correctness of parallel programs. SIAM Journal on Computing, pages 227–246, 1981.

    Google Scholar 

  18. D. Gries. The Science of Programming. Springer-Verlag, New York, 1981.

    Book  MATH  Google Scholar 

  19. C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12: 576–580, 583, 1969.

    Google Scholar 

  20. C.A.R. Hoare. Parallel programming• an axiomatic approach. Computer Languages, 1: 151–160, 1975.

    Article  MATH  Google Scholar 

  21. C.A.R. Hoare. Communicating sequential processes. Communications of the ACM, 21: 666–677, 1978.

    Article  MATH  Google Scholar 

  22. C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, NJ, 1985.

    MATH  Google Scholar 

  23. HP79] M.C.B. Hennessy and G.D. Plotkin. Full abstraction for a simple programming language. In Proceedings of Mathematical Foundations of Computer Science,pages 108–120, New York, 1979. Lecture Notes in Computer Science 74, Springer-Verlag.

    Google Scholar 

  24. INMOS Limited. Occam Programming Manual. Prentice-Hall International, Englewood Cliffs, N.J., 1984.

    Google Scholar 

  25. L. Lamport. Proving the correctness of multiprocess programs IEEE Transactions on Software Engineering, SE-3: 2: 125–143, 1977.

    MathSciNet  Google Scholar 

  26. G. Levin and D. Gries. A proof technique for communicating sequential processes. Acta Informatica, 15: 281–302, 1981.

    Article  MathSciNet  MATH  Google Scholar 

  27. R. Lipton. Reduction: a method of proving properties of parallel programs Communications of the ACM, 18: 717–721, 1975.

    Article  MathSciNet  MATH  Google Scholar 

  28. R. Milner. A Calculus of Communicating Systems. Lecture Notes in Computer Science 92, Springer-Verlag, New York, 1980.

    Google Scholar 

  29. R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, NJ, 1989.

    MATH  Google Scholar 

  30. Z. Manna and A. Pnueli. Verification of concurrent programs: the temporal framework. In R.S. Boyer and J.S. Moore, editors, The Correctness Problem in Computer Science, International Lecture Series in Computer Science, London, 1981. Academic Press.

    Google Scholar 

  31. Z. Manna and A. Pnueli. How to cook a temporal proof system for your pet language. In Proceedings of the 10th Annual ACM Symposium on Principles of Programming Languages, pages 141154, Austin, Texas, U.S.A., 1983.

    Google Scholar 

  32. Z. Manna and A. Pnueli. Adequate proof principles for invariance and liveness properties of concurrent programs. Science of Computer Programming, 4: 257–289, 1984.

    Article  MathSciNet  MATH  Google Scholar 

  33. E.-R. Olderog and K.R. Apt. Fairness in parallel programs, the transformational approach. ACM Transactions on Programming Languages and Systems, 10: 420–455, 1988.

    Article  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  35. S. Owicki and D. Gries. Verifying properties of parallel programs: an axiomatic approach. Communications of the ACM, 19: 279285, 1976.

    Google Scholar 

  36. S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems, 4: 199–223, 1982.

    Article  Google Scholar 

  37. G.D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI-FN 19, Department of Computer Science, Aarhus University, 1981.

    Google Scholar 

  38. A. Pnueli. The temporal logic of programs In Proceeding of the 18th IEEE Symposium on Foundations of Computer Science, pages 46–57, 1977.

    Google Scholar 

  39. J.-P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th International Symposium on Programming, Paris, 1981.

    Google Scholar 

  40. E. Shapiro. The family of concurrent logic programming lan- guages. ACM Computing Surveys, 21 (3): 412–510, 1989.

    Article  Google Scholar 

  41. A.M. Turing. On checking a large routine. Report of a Conference on High Speed Automatic Calculating Machines, pages 67–69, 1949. Univ. Math. Laboratory, Cambridge, 1949. (See also: F.L. Morris and C.B. Jones, An early program proof by Alan Turing, Annals of the History of Computing 6 pages 139–143, 1984).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CWI, Kruislaan 413, 1098 SJ, Amsterdam, The Netherlands

    Krzysztof R. Apt

  2. Department of Computer Science, University of Oldenburg, Ammerlander Heerstr. 114-118, 2900, Oldenburg, Germany

    Ernst-Rüdiger Olderog

Authors
  1. Krzysztof R. Apt
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ernst-Rüdiger Olderog
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer Science+Business Media New York

About this chapter

Cite this chapter

Apt, K.R., Olderog, ER. (1991). Introduction. In: Verification of Sequential and Concurrent Programs. Texts and Monographs in Computer Science. Springer, New York, NY. https://doi.org/10.1007/978-1-4757-4376-0_1

Download citation

  • DOI: https://doi.org/10.1007/978-1-4757-4376-0_1

  • Publisher Name: Springer, New York, NY

  • Print ISBN: 978-1-4757-4378-4

  • Online ISBN: 978-1-4757-4376-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation