Skip to main content
SpringerLink
Log in
Book cover

Temporal Logic in Specification pp 202–212Cite as

Unified verification theory

  • Collected Papers
  • Conference paper
  • First Online:

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

Abstract

We present an automata-theoretic framework to the verification of concurrent and nondeterministic programs. The basic idea is that to verify that a program P is correct one writes a program A that receives the computation of P as input and diverges only on incorrect computations of P. Now P is correct if and only if the program P A , which is obtained by combining P and A, terminates. This unifies previous works on verification of temporal properties and verification of fair termination.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

6 References

  1. Apt, K.R.: Ten years of Hoare's logic: a survey — Part I. ACM Trans. on Programming Languages and Systems 3(1981), pp. 431–483.

    Google Scholar 

  2. Apt, K.R.: Ten years of Hoare's logic: a survey — Part II. Theoretical Computer Science 28(1984), pp. 83–109.

    Google Scholar 

  3. Apt, K.R., Olderog, E.R.: Proof rules and transformation dealing with fairness. Science of Computer Programming 3(1983), pp. 65–100.

    Google Scholar 

  4. Apt, K.R., Plotkin, G.D.: Countable nondeterminism and random assignment. J. ACM 33(1986), pp. 724–767.

    Google Scholar 

  5. Apt, K.R., Pnueli, A., Stavi, J.: Fair termination revisited — with delay. Theoretical Computer Science 33 (1984), pp. 65–84.

    Google Scholar 

  6. Alpern, B., Schneider, F.B.: Verifying temporal properties without using temporal logic. Technical Report TR-85-723, Cornell University, Dec. 1985.

    Google Scholar 

  7. Alpern, B., Schneider, F.B.: Proving Boolean combinations of deterministic properties. To appear in Proc. 2nd IEEE Symp. on Logic in Computer Science, Ithaca, June 1987.

    Google Scholar 

  8. Boom, H.J.: A weaker precondition for loops. ACM Trans. on Programming Languages and Systems 4(1982), pp. 668–677.

    Google Scholar 

  9. Büchi, J.R.: On a decision method in restricted second-order arithmetics. Proc. Int'l Congr. on Logic, Method. and Phil. of Sci. 1960, Stanford University Press, 1962, pp. 1–12.

    Google Scholar 

  10. Choueka, Y.: Theories of automata on ω-tapes — a simplified approach. J. Computer and System Science 8(1974), pp. 117–141.

    Google Scholar 

  11. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specification. ACM Trans. on Programming Languages and Systems 8(1986), pp. 244–263.

    Google Scholar 

  12. Dayan, I., Harel, D.: Fair termination with cruel schedulers. Fundamenta Informatica 9(1986), pp. 1–12.

    Google Scholar 

  13. Francez, N.: Fairness. Text and Monographs in Computer Science, Springer-Verlag, 1986.

    Google Scholar 

  14. Grumberg, O., Francez, N., Makowsky, J.A., de Roever, W.P.: A proof rule for fair termination of guarded command. Information and Control 66(1985), pp. 83–102.

    Google Scholar 

  15. Harel, D.: Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness. J. ACM 33(1986), pp. 225–248.

    Google Scholar 

  16. Hailpern, B.T., Owicki, S.S.: Modular verification of computer communication protocols. IEEE Trans. on Comm. COM-31(1983), pp. 56–68.

    Google Scholar 

  17. Harel, D., Pnueli, A., Stavi, J.: Propositional dynamic logic of non-regular programs. J. Computer and System Sciences 26(1983) 222–243.

    Google Scholar 

  18. Lichtenstein, O., Pnueli, A.: Checking that finite-state concurrent programs satisfy their linear specification. Proc. 12th ACM Symp. on Principles of programming Languages, 1985, pp. 97–107.

    Google Scholar 

  19. Lehman, D., Pnueli, A., Stavi, J.: Impartiality, justice, and fairness — the ethic of concurrent termination. Proc. 8th Int'l Colloq. on Automata, Language, and Programming, LNCS 115, Springer-Verlag, 1981, pp. 264–277.

    Google Scholar 

  20. Z. Manna, A. Pnueli — Verification of concurrent programs: the temporal framework. In The Correctness Problem in Computer Science, (R.S. Boyer, J.S. Moore, eds.) International Lecture Series in Computer Science, Academic Press, London, 1981, 215–273.

    Google Scholar 

  21. Manna, Z., Pnueli, A.: How to cook a temporal proof system for your pet language. Proc. 10th Symposium on Principles of Programming Languages, Austin, Texas, 1983, pp. 141–154.

    Google Scholar 

  22. Manna, Z., Pnueli, A.: Proving precedence properties: The temporal way. Proc. 10 Int'l Colloq.on Automata Languages and Programming, LNCS 154, Springer Verlag, 1983, pp. 491–512.

    Google Scholar 

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

    Google Scholar 

  24. Manna, Z., Pnueli, A.: Specification and verification of concurrent programs by ∀-automata. Proc. 14 ACM Symp. on Principles of Programming Languages, Munich, Jan. 1987, pp. 1–12.

    Google Scholar 

  25. Nivat, M.: Behavior of processes and synchronized systems of processes. In Theoretical Foundations of Programming Methodology (M. Broy, G. Schmidt, eds.), Reidel, 1982, pp. 473–551.

    Google Scholar 

  26. Owicki, S.S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Trans. on Programming Languages and Systems 4(1982), pp. 455–495.

    Google Scholar 

  27. Park, D.: On the semantics of fair parallelism. Proc. Copenhagen Winter School on Abstract Software Specification, 1979, LNCS 86, Springer-Verlag.

    Google Scholar 

  28. Park, D.: A predicate transformer for weak fair termination. Proc. 6th IBM Symp. on Math. Foundations of Computer Science, Hakone, Japan, 1981.

    Google Scholar 

  29. Park, D.: Concurrency and automata on infinite sequences. Proc. 5th GI Conf. on Theoretical Computer Science, 1981, Springer-Verlag, LNCS 104, pp. 167–183.

    Google Scholar 

  30. Pnueli, A.: The temporal logic of program. Proc. 18th Symp. on Foundations of Computer Science, 1977, pp. 46–57.

    Google Scholar 

  31. Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Computer Science 13 (1981), pp. 45–60.

    Google Scholar 

  32. Queille, J.P., Sifakis, J.: Fairness and related properties in transition systems — a temporal logic to deal with fairness. Acta Informatica 19(1983), pp. 195–220.

    Google Scholar 

  33. Rogers, H.: Theory of recursive functions and effective computability. McGraw-Hill, 1967.

    Google Scholar 

  34. Rinat, R., Francez, N., Grumberg, O.: Infinite trees, markings, and well-foundedness. Proc. 11th Colloq. on Trees in Algebra and Programming (CAAP 86), LNCS 214, Springer-Verlag, pp. 238–253.

    Google Scholar 

  35. Rescher, N, Urquhart, A.: Temporal Logic. Springer-Verlag, 1971.

    Google Scholar 

  36. Streett, R.S.: Propositional dynamic logic of looping and converse. Information and Control 54(1982), pp. 121–141.

    Google Scholar 

  37. Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(1985), pp. 733–749.

    Google Scholar 

  38. Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for Büchi automata with applications to temporal logic. Proc. 12th Int'l Colloq. on Automata, Languages, and Programming, LNCS 194, Springer-Verlag, 1985, pp. 465–474. To appear in Theoretical Computer Science.

    Google Scholar 

  39. Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. Proc. 26th IEEE Symp. on Foundations of Computer Science, Portland, 1985, pp. 327–338.

    Google Scholar 

  40. Vardi, M.Y.: Verification of concurrent programs — the automata-theoretic framework. Proc. 2nd IEEE Symp. on Logic in Computer Science, Ithaca, 1987, pp. 167–176.

    Google Scholar 

  41. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. Proc. IEEE Symp. on Logic in Computer Science, Cambridge, 1986, pp. 332–344.

    Google Scholar 

  42. Wolper, P.: Temporal logic can be more expressive. Information and Control 56(1983), pp. 72–99.

    Google Scholar 

  43. Wolper, P.: Expressing interesting properties of programs in propositional temporal logic. Proc. 13th ACM Symp. on Principles of programming Languages. St. Petersburg Beach, Florida, 1986, pp. 184–193.

    Google Scholar 

  44. Wagner, K., Staiger, L.: Recursive ω-languages. Proc. Symp. on Foundation of Computation Theory, LNCS 56, Springer-Verlag, 1977, pp. 532–537.

    Google Scholar 

  45. Wolper, P.L., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. Proc. 24th IEEE Symp. on Foundation of Computer Science, Tuscon, 1983, pp. 185–194.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IBM Almaden Research K53-802, 650 Harry Rd., 95120-6099, San Jose, CA

    Moshe Y. Vardi

Authors
  1. Moshe Y. Vardi
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

B. Banieqbal H. Barringer A. Pnueli

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Vardi, M.Y. (1989). Unified verification theory. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds) Temporal Logic in Specification. Lecture Notes in Computer Science, vol 398. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51803-7_27

Download citation

  • DOI: https://doi.org/10.1007/3-540-51803-7_27

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-46811-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation