Advertisement

Proving precedence properties: The temporal way

  • Zohar Manna
  • Amir Pnueli
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 154)

Abstract

The paper explores the three important classes of temporal properties of concurrent programs: invariance, liveness and precedence. It presents the first methodological approach to the precedence properties, while providing a review of the invariance and liveness properties. The approach is based on the unless operator \(\mathfrak{A}\), which is a weak version of the until operator U. For each class of properties, we present a single complete proof principle.

Keywords

Mutual Exclusion Concurrent Program Liveness Property State Formula Temporal Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [K]
    Keller, R.M., “Formal verification of parallel programs,” CACM, Vol. 19, No. 7 (July 1976), pp. 371–384.Google Scholar
  2. [L1]
    Lamport, L., “Proving the Correctness of Multiprocess Programs,” IEEE Trans. Soft. Eng. SE-3, 2 (Mar. 1977), pp. 125–143.Google Scholar
  3. [L2]
    Lamport, L., “ 'sometime ‘is Sometimes ‘Not Never': On the Temporal Logic of Programs,” 7th Annual ACM Symposium on Principles of Programming Languages (1980), pp. 174–185.Google Scholar
  4. [LPS]
    Lehmann, D., A. Pnueli, and J. Stavi, “Impartiality, justice and fairness: the ethics of concurrent termination,” in Automata Languages and Programming, Lecture Notes in Computer Science 115, Springer Verlag (1981), pp. 264–277.Google Scholar
  5. [MP1]
    Manna, Z. and A. Pnueli, “Verification of Concurrent Prorams: The Temporal Framework,” in The Correctness Problem in Computer Science (R.S. Boyer and J S. Moore, eds.), International Lecture Series in Computer Science, Academic Press, London (1982), pp. 215–273.Google Scholar
  6. [MP2]
    Manna, Z. and A. Pnueli, “Verification of Concurrent Programs: Temporal Proof Principles,” Proc. of the Workshop on Logic of Programs (D. Kozen, ed.), Yorktown-Heights, N.Y. (1981). Springer-Verlag Lecture Notes in Computer Science 131, pp. 200–252.Google Scholar
  7. [MP3]
    Manna, Z. and A. Pnueli, “Verification of Concurrent Programs: Proving Eventualities by Well-Founded Ranking,” TOPLAS (1983, to appear).Google Scholar
  8. [MP4]
    Manna, Z. and A. Pnueli, “Verification of Concurrent Programs: a Temporal Proof System,” Proc. 4th School on Advanced Programming, Amsterdam, Holland (June 1982).Google Scholar
  9. [MP5]
    Manna, Z. and A. Pnueli, “How to Cook a Temporal Proof System for Your Pet Language,” in the Proc. of the Symposium on Principles of Programming Languages, Austin, Texas (Jan. 1983).Google Scholar
  10. [MP6]
    Manna, Z. and A. Pnueli, “Proving Precedence Properties: The Temporal Way,” Technical Report, Computer Science Dept., Stanford University, Stanford, CA(1983, to appear).Google Scholar
  11. [OL]
    Owicki, S. and L. Lamport, “Proving Liveness Properties of Concurrent Programs,” ACM Transactions on Programming Languages and Systems, Vol. 4, No. 3 (July 1982), pp. 455–495.Google Scholar
  12. [OG]
    Owicki, S. and D. Gries, “An Axiomatic Proof technique for Parallel Programs,” Acta Informatica, Vol. 6, No. 4 (1976), pp. 319–340.Google Scholar
  13. [Pe]
    Peterson, G.L., “Myths about the Mutual Exclusion Problem,” Information Processing Letters, Vol. 12, No. 3 (June 1981), pp. 115–116.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • Zohar Manna
    • 1
    • 2
  • Amir Pnueli
    • 2
  1. 1.Computer Science DepartmentStanford UniversityStanford
  2. 2.Applied Mathematics DepartmentThe Weizmann Institute of ScienceRehovotIsrael

Personalised recommendations