Formal derivation of strongly correct concurrent programs. (English) Zbl 0389.68012


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


[1] Burstall, R.: Program proving as hand simulation with a little induction. Proc. IFIP Congress 1974, Stockholm, pp. 308–312. Amsterdam: North Holland 1974 · Zbl 0299.68012
[2] de Bakker, J.W., de Roever, W.P.: A calculus for recursive program schemes. In: Automata, Languages and Programming 1 (M. Nivat, ed.), pp. 167–196. Amsterdam: North Holland 1973 · Zbl 0262.68004
[3] Devillers, R.E., Lauer, P.E.: A general mechanism for avoiding starvation with distributed control. Information Processing Lett. 7, 156–158 (1978) · Zbl 0383.68030
[4] Dijkstra, E.W.: Hierarchical ordering of sequential processes. Acta Informat. 1, 115–138 (1971)
[5] Dijkstra, E.W.: A class of allocation strategies inducing bounded delays only. Proc. SJCC 1972, pp. 933–936. Montvale, N.J.: AFIPS Press 1972
[6] Dijkstra, E.W.: A Discipline of Programming. Englewood Cliffs, N.J.: Prentice Hall, 1976 · Zbl 0368.68005
[7] Dijkstra, E.W.: Two starvation-free solutions of a general exclusion problem. Report EWD 625, Burroughs-Nuenen, The Netherlands 1977
[8] Flon, L., Suzuki, N.: Nondeterminism and the correctness of parallel programs. In: Formal Description of Programming Concepts (E.J. Neuhold, ed.), pp. 589–605. Amsterdam: North Holland 1978 · Zbl 0373.68029
[9] Floyd, R.W.: Assigning meanings to programs. In: Proc. Symp. Applied Maths., Vol. 19, Aspects of Computer Science, pp. 19–32. New York: American Mathematical Society 1967 · Zbl 0189.50204
[10] Francez, N., Pnueli, A.: A proof method for cyclic programs. Acta Informat. 9, 133–157 (1978) · Zbl 0367.68009
[11] Holt, R.C.: Comment on prevention of system deadlocks. Comm. ACM 14, 36–38 (1971) · Zbl 0215.28102
[12] Keller, R.M.: Formal verification of parallel programs. Comm. ACM 19, 371–384 (1976) · Zbl 0329.68016
[13] Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Soft. Eng. SE-3, 125–143 (1977) · Zbl 05341279
[14] Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informat. 6, 319–340 (1976) · Zbl 0324.68007
[15] Park, D.: Fixpoint induction and proofs of program properties. In: Machine Intelligence (B. Meltzer and D. Michie, eds.), Vol. 5, pp. 59–78. Edinburgh: University Press 1969 · Zbl 0219.68007
[16] Sintzoff, M.: Eliminating blind alleys from backtrack programs. In: Automata, Languages and Programming 3 (S. Michaelson and R. Milner, eds.), pp. 531–557. Edinburgh: University Press 1976 · Zbl 0362.68053
[17] Sintzoff, M.: Inventing program construction rules. In: Constructing Quality Software (P.G. Hibbard and S.A. Schuman, eds.), pp. 471–501. Amsterdam: North Holland 1978
[18] Sintzoff, M.: Ensuring correctness by arbitrary postfixed-points. In: 7th Symposium on Mathematical Foundations of Computer Science (J. Winkowski, ed.), Lecture Notes in Computer Science, Vol. 64, pp. 484–492. Berlin-Heidelberg-New York: Springer 1978 · Zbl 0412.68015
[19] Sintzoff, M., van Lamsweerde, A.: Constructing correct and efficient concurrent programs. Proceedings ACM-IEEE International Conference on Reliable Software 1975, Los Angeles. Sigplan Notices 10, 319–326 (1975)
[20] van Lamsweerde, A., Sintzoff, M.: Formal derivation of strongly correct parallel programs. MBLE Res. Lab., Brussels, Report R 338, October 1976 · Zbl 0389.68012
[21] van Lamsweerde, A.: From verifying termination to guaranteeing it: a case study. In: Formal Description of Programming Concepts (E.J. Neuhold, ed.), pp. 609–620. Amsterdam: North Holland 1978 · Zbl 0373.68027
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.