×

Axiomatic treatment of processes with shared variables revisited. (English) Zbl 0748.68040


MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)

Citations:

Zbl 0543.68010
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ashcroft, E.A.: Proving Assertions about Parallel Programs.Journal of Computer and System Sciences,10(1), 110-135 (1975). · Zbl 0299.68013
[2] Dahl, O.-J.: Time Sequences as a Tool for Describing Program Behaviour, Research Report 48, Department of Informatics, University of Oslo, Norway, 1979.
[3] Dahl, O.-J.: Parallel Programming (in Norwegian), Kompendium no. 46, Department of Informatics, University of Oslo, Norway, 1989.
[4] DÆhlin, J.H.: Semantikk om invarians og progresjon (Semantics for Safety and Liveness), Master Thesis (In Norwegian), Department of Informatics, University of Oslo, Norway, 1987.
[5] Gjessing, S. and Munthe-Kaas, E.: Trace Based Verification of Parallel Programs with Shared Variables 22nd Hawaii Int. Conf. on System Sciences, 3-6 January 1989.
[6] Hoare, C.A.R.: An Axiomatic Basis for Computer Programming,CACM,12(10), 576-583 (1969). · Zbl 0179.23105
[7] Jones, C.B.: Specification and Design of (Parallel) Programs, Proc. IFIP 9th World Computer Congress, North Holland, pp. 321-332, 1983.
[8] Kahn, G.: The Semantics of a Simple Language for Parallel Programming, Information Processing 74, North-Holland, 1974. · Zbl 0299.68007
[9] Lamport, L.: The ?Hoare Logic? of Concurrent Programs, Acta Informatica,14, 21-37 (1980). · Zbl 0428.68041
[10] Lamport, L.: Predicate Transformers for Concurrency, Technical Report, Digital System Center, CA, 1987 (Revised 1988).
[11] Manna, Z. and Pnueli, A.: Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs.Science of Computer Programming,4(3) 257-289 (1984) (and STAN-CS-84-1005). · Zbl 0542.68014
[12] Meldal, S.: On Hierarchical Abstraction and Partial Correctness of Concurrent Structures, Ph.D. thesis, Department of Informatics, University of Oslo, Norway, 1986 (also inBIT,26(2), 164-174 (1986)). · Zbl 0599.68029
[13] Meldal, S.: Private communication. Department of Informatics, University of Bergen, Norway, 1989.
[14] Owicki, S. and Gries, D.: An Axiomatic Proof Technique for Parallel Programs.Acta Informatica,6 319-340 (1976). · Zbl 0324.68007
[15] Owicki, S. and Lamport, L.: Proving Liveness Properties of Concurrent Programs.ACM Transactions on Programming Languages and Systems,4(3) 455-495 (1982). · Zbl 0483.68013
[16] Soundararajan, N. and Dahl, O.-J.: Partial Correctness Semantics of Communicating Sequential Processes, Research Report 66, Department of Informatics, University of Oslo, Norway, 1982.
[17] Soundararajan, N.: A Proof Technique for Parallel Programs.Theoretical Computer Science,31, 13-29 (1984). · Zbl 0543.68010
[18] Stirling, C.P.: A Generalization of Owicki-Gries’ Hoare Logic for a Concurrent While Language.Journal of Theoretical Computer Science,58, 347-360 (1988). · Zbl 0653.03017
[19] StØlen, K.: Development of Parallel Programs on Shared Data-Structures, Ph.D. thesis, Manchester University, Manchester, UK, 1990.
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.