How to cook a temporal proof system for your pet language

ABSTRACT

An abstract temporal proof system is presented whose program-dependent part has a high-level interface with the programming language actually studied. Given a new language, it is sufficient to deline the interface notions of atomic transitions, justice, and fairness in order to obtain a full temporal proof system for this language. This construction is particularly useful for the analysis of concurrent systems. We illustrate the construction on the shared-variable model and on CSP. The generic proof system is shown to be relatively complete with respect to pure first-order temporal logic.

REFERENCES

• 1: {B} Ben-Ari, M., "Temporal Logic Proofs of Concurrent Programs," Technical Report, Tel Aviv University (1981).
• 2: C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
• 3: {KR} Kuiper, R. and de Roever, W. P., "Fairness Assumptions for CSP in a Temporal Logic Framework," TC2 Working Conference on the Formal Description of Programming Concepts, Garmisch (June 1982).
• 4: {M} Manna, Z., "Verification of Sequential Programs: Temporal Axiomatization," Theoretical Foundations of Programming Methodology (M. Broy and G. Schmidt, eds.), NATO Scientific Series, D. Reidel Pub. Co., Holland (1982), pp. 53-102.
• 5: {MP1} Manna, Z. and Pnueli, A., "Verification of Concurrent Programs: 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. 215273.
• 6: {MP2} Manna, Z. and Pnueli, A., "Verification of Concur rent Programs: a Temporal Proof System," Proc. 4th School on Advanced Programming, Amsterdam, Holland (June 1982).
• 7: Zohar Manna , Amir Pnueli, Verification of Concurrent Programs: Temporal Proof Principles, Logic of Programs, Workshop, p.200-252, May 01, 1981
• 8: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 9: {P} Pnueli, A., "The Temporal Semantics of Concurrent Programs," Theoretical Computer Science 13 (1981), pp. 45-60.
• 10: {PR} Pnueli, A. and de Roever, W. P., "Rendezvous with ADA --- A Proof Theoretical View," Proc. of the AdaTEC Conference, Crystal City (1982).
• 11: {SM} Schwartz, R. L. and Melliar-Smith, P. M., "Temporal Logic Specifications of Distributed Systems," Proc. of the 2nd International Conference on Distributed Computing Systems, Paris, France (1981).