The temporal semantics of concurrent programs. (English) Zbl 0441.68010


68Q60 Specification and verification (program logics, model checking, etc.)
68N25 Theory of operating systems
Full Text: DOI


[1] Ashcroft, E. A., Proving assertions about parallel programs, J. Comput. System Sci., 10, 1, 110-135 (1975) · Zbl 0299.68013
[2] Ashcroft, E. A.; Wadge, W. W., Intermittent assertion proofs in lucid, (Gilchrist, B., Information Processing, 77 (1977), North-Holland: North-Holland Amsterdam), 723-726 · Zbl 0363.68021
[3] Brinch Hansen, P., A comparison of two synchronizing concepts, Acta Informat., 1, 190-199 (1972) · Zbl 0226.68027
[4] Büchi, J. R., On a decision method in restricted second order arithmetic, Stanford, CA. Stanford, CA, International Congress on Logic Methodology and Philosophy of Science (1960) · Zbl 0142.24902
[5] Bull, R. A., An algebraic study of Diodorean modal systems, J. Symbolic Logic, 30, 58-64 (1965) · Zbl 0129.25707
[6] Burstall, R. M., Formal description of program structure and semantics of first order logic, Machine Intelligence, 5, 79-98 (1970) · Zbl 0221.68018
[7] Dummet, M. A.; Lemmon, E. J., Modal logic between \(S4\) and \(S5\), Z. Math. Logik Grundlagen Math., 5, 250-264 (1959) · Zbl 0178.30801
[8] Francez, N.; Pnueli, A., The analysis of cyclic programs, Acta Informat., 9, 133-157 (1978) · Zbl 0367.68009
[9] D. Gries, A proof of correctness of Reim’s semaphore implementation of the With — When; D. Gries, A proof of correctness of Reim’s semaphore implementation of the With — When
[10] Harel, D.; Pratt, V. R., Nondeterminism in logics of programs, Tucson, AZ. Tucson, AZ, Proc. 5th ACM Symposium on Principles of Programming Languages (1978)
[11] Hoare, C. A.R., Towards a theory of parallel programming, (Hoare; Perrot, Operating Systems Techniques (1972), Academic Press: Academic Press New York), 61-71 · Zbl 0951.01025
[12] Hughes, G. E.; Creswell, M. J., An Introduction to Modal Logic (1972), Methuen: Methuen London
[13] Kahn, G., The semantics of simple language for parallel programming, (Rosenfeld, J. L., Information Processing, 74 (1974), North-Holland: North-Holland Amsterdam), 471-475 · Zbl 0299.68007
[14] Keller, R. M., Formal verification of parallel programs, Comm. ACM, 19, 7, 371-384 (1976) · Zbl 0329.68016
[15] L. Krablin, A temporal analysis of fairness, a forthcoming M.Sc. thesis, University of Pennsylvania.; L. Krablin, A temporal analysis of fairness, a forthcoming M.Sc. thesis, University of Pennsylvania.
[16] Kröger, F., LAR: a logic of algorithmic reasoning, Acta Informat., 8, 243-266 (1977) · Zbl 0347.68016
[17] Lamport, L., Proving the correctness of multiprocess programs, IEEE Trans. Software Engrg., 3, 2, 125-143 (1977) · Zbl 0349.68006
[18] Lamport, L., Sometime is sometimes ‘not never’, (Technical Report CSL-86 (1979), SRI International: SRI International Menlo Park, CA)
[19] Manna, Z., Properties of programs and first order predicate calculus, J. ACM, 16, 2, 244-255 (1969) · Zbl 0198.22001
[20] Owicki, S.; Gries, D., An axiomatic proof technique for parallel programs, Acta Informat., 5, 319-339 (1975) · Zbl 0312.68011
[21] Owicki, S.; Gries, D., Verifying properties of parallel programs: An axiomatic approach, Comm. ACM, 19, 5, 279-284 (1976) · Zbl 0322.68010
[22] Pnueli, A., The temporal logic of programs, Providence RI. Providence RI, Proc. 19th Annual Symposium on Foundations of Computer Science (1977)
[23] Prior, A., Past, Present and Future (1967), Oxford University Press: Oxford University Press London · Zbl 0169.29802
[24] Gabbay, D.; Pnueli, A.; Shelah, S.; Stavi, J., The temporal analysis of fairness, Las Vegas. Las Vegas, 7th Annual Symposium on Principles of Programming Languages (1980)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.