{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:29:15Z","timestamp":1742912955554,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540092513"},{"type":"electronic","value":"9783540353126"}],"license":[{"start":{"date-parts":[[1979,1,1]],"date-time":"1979-01-01T00:00:00Z","timestamp":283996800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[1979,1,1]],"date-time":"1979-01-01T00:00:00Z","timestamp":283996800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1979]]},"DOI":"10.1007\/bfb0014668","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T05:25:49Z","timestamp":1132723549000},"page":"174-197","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Specifications and proofs for abstract data types in concurrent programs"],"prefix":"10.1007","author":[{"given":"Susan S.","family":"Owicki","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"19_CR1","volume-title":"Operating Systems Principles","author":"P. Brinch Hansen","year":"1973","unstructured":"P. Brinch Hansen. Operating Systems Principles. Prentice Hall, Englewood Cliffs, New Jersey, (1973)."},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"P. Brinch Hansen. The programming language concurrent Pascal. IEEE Trans. on Software Eng., SE-1 No. 2, (June, 1975), pp. 199\u2013207.","DOI":"10.1109\/TSE.1975.6312840"},{"key":"19_CR3","unstructured":"D.I. Good and A.L. Ambler. Proving systems of concurrent processes synchronized with message buffers. Draft, (1975)."},{"key":"19_CR4","unstructured":"J.V. Guttag. The specification and application to programming of abstract data types. Ph.D. thesis, Computer Science, University of Toronto, (Sept. 1975)."},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"J.V. Guttag, E. Horowitz, D.R. Musser. Abstract data types and software validation. Univ. of Southern California Information Sciences Institute report 76\u201348, (August, 1976).","DOI":"10.21236\/ADA029896"},{"issue":"10","key":"19_CR6","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"C.A.R. Hoare. An axiomatic basis for computer programming. Comm. ACM 12, 10 (Oct. 1969), pp. 576\u2013583.","journal-title":"Comm. ACM"},{"key":"19_CR7","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/BFb0059696","volume-title":"Symp. on the Semantics of Algorithmic Languages","author":"C.A.R. Hoare","year":"1971","unstructured":"C.A.R. Hoare. Procedures and parameters\u2014an axiomatic approach. Symp. on the Semantics of Algorithmic Languages, Springer, Berlin-Heidelberg-New York, (1971), pp. 102\u2013116."},{"key":"19_CR8","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1972","unstructured":"C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica 1 (1972), pp. 271\u2013281.","journal-title":"Acta Informatica"},{"issue":"3","key":"19_CR9","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1093\/comjnl\/16.3.209","volume":"16","author":"C.A.R. Hoare","year":"1973","unstructured":"C.A.R. Hoare. A structured paging system. Computer J. 16, 3 (1973), pp. 209\u2013215.","journal-title":"Computer J."},{"issue":"10","key":"19_CR10","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1145\/355620.361161","volume":"17","author":"C.A.R. Hoare","year":"1974","unstructured":"C.A.R. Hoare. Monitors: an operating system structuring concept. Comm. ACM 17, 10 (Oct. 1974), pp. 549\u2013556.","journal-title":"Comm. ACM"},{"issue":"5","key":"19_CR11","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/360051.360079","volume":"19","author":"J.H. Howard","year":"1976","unstructured":"J.H. Howard. Proving monitors. Comm. ACM 19, 5 (May 1976), pp. 273\u2013279.","journal-title":"Comm. ACM"},{"key":"19_CR12","unstructured":"L. Lamport. Formal correctness proofs for multiprocess algorithms. Proc. Second Int. Symp. on Programming, April 1976."},{"key":"19_CR13","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1109\/TSE.1975.6312816","volume":"1","author":"B.H. Liskov","year":"1975","unstructured":"B.H. Liskov and S. Zilles. Specification techniques for data abstractions. IEEE Trans. on Software Eng. SE-1, 1 (March 1975), pp. 7\u201319.","journal-title":"IEEE Trans. on Software Eng."},{"key":"19_CR14","unstructured":"B.H. Liskov and V. Berzins. An appraisal of program specifications. Computation Structures Group Memo 141, M.I.T. (July 1976)."},{"key":"19_CR15","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/BF00288637","volume":"3","author":"Z. Manna","year":"1974","unstructured":"Z. Manna and A. Pnueli. Axiomatic approach to total correctness of programs. Acta Informatica 3 (1974) pp. 243\u2013263.","journal-title":"Acta Informatica"},{"key":"19_CR16","volume-title":"A provably secure operating system","author":"P.G. Neumann","year":"1975","unstructured":"P.G. Neumann, L. Robinson, K.N. Levitt, R.S. Boyer, A.R. Saxena. A provably secure operating system. Stanford Research Institute, Menlo Park, California (June 1975)."},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"S.S. Owicki. A consistent and complete deductive system for the verification of parallel programs. Proc. 8thACM Symp. on Theory of Computing, (May 1976), pp. 73\u201386.","DOI":"10.1145\/800113.803634"},{"issue":"5","key":"19_CR18","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1145\/360051.360224","volume":"19","author":"S.S. Owicki","year":"1976","unstructured":"S.S. Owicki and D. Gries. Verifying properties of parallel programs: an axiomatic approach. Comm. ACM 19, 5 (May 1976), pp. 280\u2013285.","journal-title":"Comm. ACM"},{"key":"19_CR19","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S.S. Owicki","year":"1976","unstructured":"S.S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I, Acta Informatica 6 (1976) pp. 319\u2013340.","journal-title":"Acta Informatica"},{"issue":"5","key":"19_CR20","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1145\/355602.361309","volume":"15","author":"D.L. Parnas","year":"1972","unstructured":"D.L. Parnas. A technique for the specification of software modules, with examples. Comm. ACM 15, 5 (May 1972), pp. 330\u2013336.","journal-title":"Comm. ACM"},{"key":"19_CR21","unstructured":"V. Schorre. A program verifier with assertions in terms of abstract data. Systems Development Corporation report SP 3841, Santa Monica, California."},{"key":"19_CR22","unstructured":"M. Shaw. Abstraction and verification in Alphard: design and verification of a tree handler. Computer Science Department, Carnegie-Mellon University, (June 1976)."},{"key":"19_CR23","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/BF00288745","volume":"4","author":"J. Spitzen","year":"1975","unstructured":"J. Spitzen and B. Wegbreit. The verification and synthesis of data structures. Acta Informatica 4 (1975), pp. 127\u2013144.","journal-title":"Acta Informatica"},{"key":"19_CR24","first-page":"253","volume":"4","author":"W.A. Wulf","year":"1976","unstructured":"W.A. Wulf, R.L. London, and M. Shaw. An introduction to the construction and verification of Alphard programs. IEEE Trans. on Software Eng., SE-2, 4 (December, 1976), pp. 253\u2013265.","journal-title":"IEEE Trans. on"}],"container-title":["Lecture Notes in Computer Science","Program Construction"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014668","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,19]],"date-time":"2022-08-19T05:03:54Z","timestamp":1660885434000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/BFb0014668"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1979]]},"ISBN":["9783540092513","9783540353126"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/bfb0014668","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1979]]},"assertion":[{"value":"9 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}