{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:14:30Z","timestamp":1725664470822},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540592938"},{"type":"electronic","value":"9783540492337"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59293-8_238","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:13:15Z","timestamp":1330276395000},"page":"795-796","source":"Crossref","is-referenced-by-count":0,"title":["The HOL-UNITY verification system"],"prefix":"10.1007","author":[{"given":"Flemming","family":"Andersen","sequence":"first","affiliation":[]},{"given":"Ulla","family":"Binau","sequence":"additional","affiliation":[]},{"given":"Karsten","family":"Nyblad","sequence":"additional","affiliation":[]},{"given":"Kim Dam","family":"Petersen","sequence":"additional","affiliation":[]},{"given":"Jimmi S.","family":"Pettersson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"55_CR1","doi-asserted-by":"crossref","unstructured":"K. Mani Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"55_CR2","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL. A theorem proving environment for higher order logic. Cambridge University Press, Computer Laboratory, 1993."},{"key":"55_CR3","unstructured":"K. Slind. HOL90 Users Manual. Technical report, 1992."},{"issue":"2","key":"55_CR4","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/BF01898402","volume":"3","author":"B. A. Sanders","year":"1991","unstructured":"Beverly A. Sanders. Eliminating the Substitution Axiom from UNITY Logic. Formal Aspects of Computing, 3(2):189\u2013205, April\u2013June 1991.","journal-title":"Formal Aspects of Computing"},{"key":"55_CR5","unstructured":"Flemming Andersen. A Theorem Prover for UNITY in Higher Order Logic. PhD thesis, Technical University of Denmark, 1992. Also published as TFL RT 1992-3, Tele Danmark Research, 1992."},{"key":"55_CR6","first-page":"1","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"Flemming Andersen","year":"1994","unstructured":"F. Andersen, K.D. Petersen, and J.S. Pettersson. Program Verification using HOL-UNITY. In Higher Order Logic Theorem Proving and Its Applications, 6th International Workshop, HUG'93, LNCS 780, pages 1\u201315, 1993."},{"key":"55_CR7","doi-asserted-by":"crossref","unstructured":"F. Andersen, K.D. Petersen, and J.S. Pettersson. A Graphical Tool for Proving Progress. In Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, HUG'94, LNCS 859, pages 17\u201332, 1994.","DOI":"10.1007\/3-540-58450-1_32"},{"key":"55_CR8","first-page":"66","volume":"1\u20132","author":"F. Andersen","year":"1993","unstructured":"F. Andersen, K.D. Petersen, and J.S. Pettersson. Verification of Software. Teleteknik, Vol. 1\u20132, 1993, English Edition. Pages 66\u201375.","journal-title":"Teleteknik"},{"key":"55_CR9","unstructured":"U. Binau. Correct Concurrent Programs: A UNITY design method for Compositional C++ programs. PhD thesis, Technical University of Denmark, 1994."},{"key":"55_CR10","unstructured":"U. Binau. Mechanical Verification of a CC++ Mutual Exclusion Program in HOL-UNITY. Technical report in preparation, Tele Danmark Research, 1994."},{"key":"55_CR11","unstructured":"K.D. Petersen and J.S. Pettersson. Proving Protocols Correct \u2014 Proving Safety and Progress Properties of the Sliding Window Protocol using HOL-UNITY. Research Report TFL RR 1993-3, Tele Danmark Research, December 1993."}],"container-title":["Lecture Notes in Computer Science","TAPSOFT '95: Theory and Practice of Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59293-8_238.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:26:46Z","timestamp":1605648406000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59293-8_238"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540592938","9783540492337"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-59293-8_238","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}