{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,13]],"date-time":"2025-03-13T23:40:18Z","timestamp":1741909218405,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615873"},{"type":"electronic","value":"9783540706410"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105408","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T21:17:00Z","timestamp":1320873420000},"page":"235-250","source":"Crossref","is-referenced-by-count":2,"title":["Towards applying the composition principle to verify a microkernel operating system"],"prefix":"10.1007","author":[{"given":"Mark R.","family":"Heckman","sequence":"first","affiliation":[]},{"given":"Cui","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Brian R.","family":"Becker","sequence":"additional","affiliation":[]},{"given":"Dave","family":"Peticolas","sequence":"additional","affiliation":[]},{"given":"Karl N.","family":"Levitt","sequence":"additional","affiliation":[]},{"given":"Ron A.","family":"Olsson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"Mart\u00edn Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 82:253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"16_CR2","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"Mart\u00edn Abadi and Leslie Lamport. Composing specifications. ACM Transactions on Programming Languages and Systems, 15(3):73\u2013132, January 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"16_CR3","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M. Abadi","year":"1995","unstructured":"Mart\u00edn Abadi and Leslie Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507\u2013534, May 1995.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"11","key":"16_CR4","doi-asserted-by":"publisher","first-page":"1382","DOI":"10.1109\/32.41331","volume":"15","author":"W. R. Bevier","year":"1989","unstructured":"Willam R. Bevier. Kit: A study in operating system verification. IEEE Transactions on Software Engineering, 15(11):1382\u20131396, November 1989.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"16_CR5","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/BF00243131","volume":"5","author":"W. R. Bevier","year":"1989","unstructured":"William R. Bevier, Warren A. Hunt, Jr., J. Strother Moore, and William D. Young. An approach to systems verification. Journal of Automated Reasoning, 5:411\u2013428, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Pierre Collette. Application of the composition principle to unity-like specifications. In M.-C. Gaudel and J.-P. Jouannaud, editors, TAPSOFT\u2019 93: Theory and Practice of Software Development, number 668 in Lecture Notes in Computer Science, pages 230\u2013242. Springer-Verlag, April 1993.","DOI":"10.1007\/3-540-56610-4_67"},{"key":"16_CR7","unstructured":"M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higer Order Logic. Cambridge University Press, 1993."},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Judith A. Hemenway and Dr. Jonathan Fellows. Applying the Abadi-Lamport composition theorem in real-world secure system integration environments. In Proceedings of the Tenth Annual Computer Security Applications Conference, pages 44\u201353, December 1994.","DOI":"10.1109\/CSAC.1994.367294"},{"issue":"1","key":"16_CR9","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/63238.63240","volume":"32","author":"L. Lamport","year":"1989","unstructured":"Leslie Lamport. A simple approach to specifying concurrent systems. Communications of the ACM, 32(1):32\u201345, January 1989.","journal-title":"Communications of the ACM"},{"issue":"3","key":"16_CR10","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872\u2013923, May 1994.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"16_CR11","unstructured":"C. Zhang, R. Shaw, M. R. Heckman, G. D. Benson, M. Archer, K. Levitt, and R. A. Olsson. Towards a formal verification of a secure distributed system and its applications. In Proceedings of the 17th National Computer Security Conference, Baltimore, October 1994."},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"C. Zhang, R. Shaw, R. Olsson, K. Levitt, M. Archer, M. Heckman, and G. Benson. Mechanizing a programming logic for the concurrent programming language microSR in HOL. In Proceedings of the International Higher-Order-Logic Theorem Proving Workshop, pages 31\u201344, Vancouver, B.C., August 1993.","DOI":"10.1007\/3-540-57826-9_123"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Cui Zhang, Brian R. Becker, Mark R. Heckman, Karl Levitt, and Ron A. Olsson. A hierarchical method for reasoning about distributed programming languages. In E. Thomas Schubert, Phillip J. Windley, and James Alves-Foss, editors, Higher-Order-Logic Theorem Proving and Its Applications: 8th International Workshop, number 668 in Lecture Notes in Computer Science, pages 385\u2013400, Aspen Grove, Utah, September 1995. Springer-Verlag.","DOI":"10.1007\/3-540-60275-5_78"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0105408","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,13]],"date-time":"2025-03-13T23:11:27Z","timestamp":1741907487000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105408"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/bfb0105408","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}