{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:55:52Z","timestamp":1725551752720},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540297970"},{"type":"electronic","value":"9783540322504"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11576280_27","type":"book-chapter","created":{"date-parts":[[2005,10,24]],"date-time":"2005-10-24T14:01:26Z","timestamp":1130162486000},"page":"390-404","source":"Crossref","is-referenced-by-count":6,"title":["Incremental Verification of Owicki\/Gries Proof Outlines Using PVS"],"prefix":"10.1007","author":[{"given":"Arjan J.","family":"Mooij","sequence":"first","affiliation":[]},{"given":"Wieger","family":"Wesselink","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","unstructured":"\u00c1brah\u00e1m, E.: An Assertional Proof System for Multithreaded Java - Theory and Tool Support. PhD thesis, Universiteit Leiden (2005)"},{"key":"27_CR2","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"27_CR3","unstructured":"Franssen, M.: Cocktail: A tool for deriving correct programs. In: Workshop on Automated Reasoning (April 1999)"},{"key":"27_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3126-2","volume-title":"On a method of multiprogramming","author":"W.H.J. Feijen","year":"1999","unstructured":"Feijen, W.H.J., van Gasteren, A.J.M.: On a method of multiprogramming. Springer, Heidelberg (1999)"},{"key":"27_CR5","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s00446-004-0115-2","volume":"17","author":"H. Gao","year":"2005","unstructured":"Gao, H., Groote, J.F., Hesselink, W.H.: Lock-free dynamic hash tables with open addressing. Distributed Computing\u00a017, 21\u201342 (2005)","journal-title":"Distributed Computing"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/BFb0055133","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Griffioen","year":"1998","unstructured":"Griffioen, D., Huisman, M.: A comparison of PVS and Isabelle\/HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 123\u2013142. Springer, Heidelberg (1998)"},{"key":"27_CR7","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/S0020-0190(98)00158-6","volume":"68","author":"W.H. Hesselink","year":"1998","unstructured":"Hesselink, W.H.: Invariants for the construction of a handshake register. Information Processing Letters\u00a068, 173\u2013177 (1998)","journal-title":"Information Processing Letters"},{"issue":"10","key":"27_CR8","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"27_CR9","series-title":"BISS Monographs","first-page":"120","volume-title":"Workshop on Tool Support for System Development and Verification","author":"J. Hooman","year":"1998","unstructured":"Hooman, J.: Developing proof rules for distributed real-time systems with PVS. In: Workshop on Tool Support for System Development and Verification. BISS Monographs, vol.\u00a01, pp. 120\u2013139. Shaker, Aachen (1998)"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Poll, E.: Java program verification at Nijmegen: Developments and perspective. Report NIII-R0318, University of Nijmegen (2003)","DOI":"10.1007\/978-3-540-37621-7_7"},{"key":"27_CR11","unstructured":"Mooij, A.J.: Formal derivations of non-blocking multiprograms. Computer Science Report 02-13, Technische Universiteit Eindhoven (October 2002)"},{"key":"27_CR12","unstructured":"Mooij, A.J., Wesselink, W.: A formal analysis of a dynamic distributed spanning tree algorithm. Computer Science Report 03-16, Technische Universiteit Eindhoven (December 2003)"},{"key":"27_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-540-49020-3_13","volume-title":"Fundamental Approaches to Software Engineering","author":"T. Nipkow","year":"1999","unstructured":"Nipkow, T., Nieto, L.P.: Owicki\/Gries in Isabelle\/HOL. In: Finance, J.-P. (ed.) FASE 1999. LNCS, vol.\u00a01577, pp. 188\u2013203. Springer, Heidelberg (1999)"},{"key":"27_CR14","doi-asserted-by":"publisher","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 Informatica\u00a06, 319\u2013340 (1976)","journal-title":"Acta Informatica"},{"key":"27_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"27_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. In: Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Nieto, L.P.: Verification of Parallel Programs with the Owicki-Gries and Rely-Guarantee Methods in Isabelle\/HOL. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2002)","DOI":"10.1007\/3-540-36575-3_24"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"Xu, Q., de Roever, W.-P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 149\u2013174 (1997)","DOI":"10.1007\/BF01211617"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11576280_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:59:35Z","timestamp":1605643175000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11576280_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540297970","9783540322504"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/11576280_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}