{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,1]],"date-time":"2023-02-01T16:12:37Z","timestamp":1675267957733},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1979,6,1]],"date-time":"1979-06-01T00:00:00Z","timestamp":297043200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[1979,6]]},"DOI":"10.1007\/bf00264015","type":"journal-article","created":{"date-parts":[[2006,2,23]],"date-time":"2006-02-23T00:38:38Z","timestamp":1140655118000},"page":"1-31","source":"Crossref","is-referenced-by-count":35,"title":["Formal derivation of strongly correct concurrent programs"],"prefix":"10.1007","volume":"12","author":[{"given":"Axel","family":"van Lamsweerde","sequence":"first","affiliation":[]},{"given":"Michel","family":"Sintzoff","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"BF00264015_CR1","first-page":"308","volume-title":"Proc. IFIP Congress 1974, Stockholm","author":"R. Burstall","year":"1974","unstructured":"Burstall, R.: Program proving as hand simulation with a little induction. Proc. IFIP Congress 1974, Stockholm, pp. 308\u2013312. Amsterdam: North Holland 1974"},{"key":"BF00264015_CR2","first-page":"167","volume-title":"Automata, Languages and Programming 1","author":"J.W. Bakker de","year":"1973","unstructured":"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\u2013196. Amsterdam: North Holland 1973"},{"key":"BF00264015_CR3","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1016\/0020-0190(78)90082-0","volume":"7","author":"R.E. Devillers","year":"1978","unstructured":"Devillers, R.E., Lauer, P.E.: A general mechanism for avoiding starvation with distributed control. Information Processing Lett. 7, 156\u2013158 (1978)","journal-title":"Information Processing Lett."},{"key":"BF00264015_CR4","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/BF00289519","volume":"1","author":"E.W. Dijkstra","year":"1971","unstructured":"Dijkstra, E.W.: Hierarchical ordering of sequential processes. Acta Informat. 1, 115\u2013138 (1971)","journal-title":"Acta Informat."},{"key":"BF00264015_CR5","first-page":"933","volume-title":"Proc. SJCC 1972","author":"E.W. Dijkstra","year":"1972","unstructured":"Dijkstra, E.W.: A class of allocation strategies inducing bounded delays only. Proc. SJCC 1972, pp. 933\u2013936. Montvale, N.J.: AFIPS Press 1972"},{"key":"BF00264015_CR6","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Englewood Cliffs, N.J.: Prentice Hall, 1976"},{"key":"BF00264015_CR7","series-title":"Report EWD 625","volume-title":"Two starvation-free solutions of a general exclusion problem","author":"E.W. Dijkstra","year":"1977","unstructured":"Dijkstra, E.W.: Two starvation-free solutions of a general exclusion problem. Report EWD 625, Burroughs-Nuenen, The Netherlands 1977"},{"key":"BF00264015_CR8","first-page":"589","volume-title":"Formal Description of Programming Concepts","author":"L. Flon","year":"1978","unstructured":"Flon, L., Suzuki, N.: Nondeterminism and the correctness of parallel programs. In: Formal Description of Programming Concepts (E.J. Neuhold, ed.), pp. 589\u2013605. Amsterdam: North Holland 1978"},{"key":"BF00264015_CR9","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume-title":"Proc. Symp. Applied Maths., Vol. 19, Aspects of Computer Science","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proc. Symp. Applied Maths., Vol. 19, Aspects of Computer Science, pp. 19\u201332. New York: American Mathematical Society 1967"},{"key":"BF00264015_CR10","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/BF00289074","volume":"9","author":"N. Francez","year":"1978","unstructured":"Francez, N., Pnueli, A.: A proof method for cyclic programs. Acta Informat. 9, 133\u2013157 (1978)","journal-title":"Acta Informat."},{"key":"BF00264015_CR11","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/362452.362486","volume":"14","author":"R.C. Holt","year":"1971","unstructured":"Holt, R.C.: Comment on prevention of system deadlocks. Comm. ACM 14, 36\u201338 (1971)","journal-title":"Comm. ACM"},{"key":"BF00264015_CR12","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1145\/360248.360251","volume":"19","author":"R.M. Keller","year":"1976","unstructured":"Keller, R.M.: Formal verification of parallel programs. Comm. ACM 19, 371\u2013384 (1976)","journal-title":"Comm. ACM"},{"key":"BF00264015_CR13","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"SE-3","author":"L. Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Soft. Eng. SE-3, 125\u2013143 (1977)","journal-title":"IEEE Trans. Soft. Eng."},{"key":"BF00264015_CR14","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informat. 6, 319\u2013340 (1976)","journal-title":"Acta Informat."},{"key":"BF00264015_CR15","first-page":"59","volume-title":"Machine Intelligence","author":"D. Park","year":"1969","unstructured":"Park, D.: Fixpoint induction and proofs of program properties. In: Machine Intelligence (B. Meltzer and D. Michie, eds.), Vol. 5, pp. 59\u201378. Edinburgh: University Press 1969"},{"key":"BF00264015_CR16","first-page":"531","volume-title":"Automata, Languages and Programming 3","author":"M. Sintzoff","year":"1976","unstructured":"Sintzoff, M.: Eliminating blind alleys from backtrack programs. In: Automata, Languages and Programming 3 (S. Michaelson and R. Milner, eds.), pp. 531\u2013557. Edinburgh: University Press 1976"},{"key":"BF00264015_CR17","first-page":"471","volume-title":"Constructing Quality Software","author":"M. Sintzoff","year":"1978","unstructured":"Sintzoff, M.: Inventing program construction rules. In: Constructing Quality Software (P.G. Hibbard and S.A. Schuman, eds.), pp. 471\u2013501. Amsterdam: North Holland 1978"},{"key":"BF00264015_CR18","series-title":"Lecture Notes in Computer Science, Vol. 64","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1007\/3-540-08921-7_96","volume-title":"7th Symposium on Mathematical Foundations of Computer Science","author":"M. Sintzoff","year":"1978","unstructured":"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\u2013492. Berlin-Heidelberg-New York: Springer 1978"},{"key":"BF00264015_CR19","doi-asserted-by":"crossref","unstructured":"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\u2013326 (1975)","DOI":"10.1145\/390016.808454"},{"key":"BF00264015_CR20","series-title":"Report R 338","volume-title":"Formal derivation of strongly correct parallel programs","author":"A. Lamsweerde van","year":"1976","unstructured":"van Lamsweerde, A., Sintzoff, M.: Formal derivation of strongly correct parallel programs. MBLE Res. Lab., Brussels, Report R 338, October 1976"},{"key":"BF00264015_CR21","first-page":"609","volume-title":"Formal Description of Programming Concepts","author":"A. Lamsweerde van","year":"1978","unstructured":"van Lamsweerde, A.: From verifying termination to guaranteeing it: a case study. In: Formal Description of Programming Concepts (E.J. Neuhold, ed.), pp. 609\u2013620. Amsterdam: North Holland 1978"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00264015.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00264015\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00264015","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,3]],"date-time":"2019-04-03T13:14:40Z","timestamp":1554297280000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00264015"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1979,6]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1979,6]]}},"alternative-id":["BF00264015"],"URL":"https:\/\/doi.org\/10.1007\/bf00264015","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[1979,6]]}}}