Now you may compose temporal logic specifications

ABSTRACT

A compositional temporal logic proof system for the specification and verification of concurrent programs is presented. Versions of the system are developed for shared variables and communication based programming languages that include procedures.

REFERENCES

• 1: Krzysztof R. Apt , Nissim Francez , Willem P. de Roever, A Proof System for Communicating Sequential Processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.359-385, July 1980 [doi>10.1145/357103.357110]
• 2: Barringer, II. and Kuiper, R., A Temporal Logic Specification Method Supporting Hierarchical Development, Manuscript, University of Manchester (November 1983).
• 3: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 4: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 5: Hoare, C.A.R., A Calculus of Total Correctness for Communicating Processes, Science of Computer Programming, 1 1 (1981) pp. 49-72.
• 6: Harel, D., Kozen, D. and Parikh, R., Process Logic: Expressiveness, Decidability and Completeness, JCSS vol. 25 (1982) pp. 144-170.
• 7: Joseph Y. Halpern , Zohar Manna , Ben C. Moszkowski, A Hardware Semantics Based on Temporal Intervals, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.278-291, July 18-22, 1983
• 8: Jones, C.B., Specification and Design of (Parallel) Programs, Proceedings of IFIP, North Holland, Paris (Nov. 1983) pp. 321-332.
• 9: Lamport, L., The 'Hoare' Logic of Concurrent Programs, Acta Informatica 14 (1980) pp. 21-37.
• 10: J. Misra , K. M. Chandy , Todd Smith, Proving safety and liveness of communicating processes with examples, Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of distributed computing, p.201-208, August 18-20, 1982, Ottawa, Canada [doi>10.1145/800220.806698]
• 11: Manna, Z. and Pnueli, A., Verification of Concurrent Programs: The Temporal Framework, in the “Correctness Problem in Computer Science", ed. R.S. Boyer and J.S. Moore, *Academic Press, London 1982, pp. 215-273.
• 12: Zohar Manna , Amir Pnueli, How to cook a temporal proof system for your pet language, Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.141-154, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567082]
• 13: Manna, Z. and Pnueli, A., Verification of Concurrent Programs: A Temporal Proof System, in "Foundations of Computer Science IV", J.W. DeBakker and J. Van Leeuwen, editors,Mathematical Centre Tracts #159, Amsterdam (1983) pp. 163-255.
• 14: Owicki, S. and Gries, D., An Axiomatic Proof Technique for Parallel Programs, Acta Informatica 6 (1976) pp. 319-340.
• 15: Pnueli, A., The Temporal Semantics of Concurrent Programs, Theoretical Computer Science, 13 (1981) pp. 45-60.
• 16: Wolper, P., Temporal Logic can be More Expressive, 22nd Annual Symp. on Foundations of Computer Science (1981) pp. 340-347.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Temporal logic

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

General Terms:
Theory, Verification