{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T12:15:39Z","timestamp":1725624939558},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642338250"},{"type":"electronic","value":"9783642338267"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33826-7_23","type":"book-chapter","created":{"date-parts":[[2012,9,25]],"date-time":"2012-09-25T22:46:25Z","timestamp":1348613185000},"page":"333-341","source":"Crossref","is-referenced-by-count":5,"title":["Extensible Specifications for Automatic Re-use of Specifications and Proofs"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Matichuk","sequence":"first","affiliation":[]},{"given":"Toby","family":"Murray","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/3-540-44880-2_4","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"S. Blazy","year":"2003","unstructured":"Blazy, S., Gervais, F., Laleau, R.: Reuse of Specification Patterns with the B Method. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol.\u00a02651, pp. 40\u201357. Springer, Heidelberg (2003)"},{"key":"23_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-540-71067-7_16","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Cock","year":"2008","unstructured":"Cock, D., Klein, G., Sewell, T.: Secure Microkernels, State Monads and Scalable Refinement. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 167\u2013182. Springer, Heidelberg (2008)"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/BFb0053381","volume-title":"ECOOP \u201997 - Object-Oriented Programming","author":"G. Kiczales","year":"1997","unstructured":"Kiczales, G., Lamping, J., Mendhekar, A., Maeda, C., Lopes, C., Loingtier, J.-M., Irwin, J.: Aspect-Oriented Programming. In: Aksit, M., Auletta, V. (eds.) ECOOP 1997. LNCS, vol.\u00a01241, pp. 220\u2013242. Springer, Heidelberg (1997)"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: 22nd SOSP, Big Sky, MT, USA, pp. 207\u2013220. ACM (October 2009)","DOI":"10.1145\/1629575.1629596"},{"key":"23_CR5","unstructured":"Klein, G., Murray, T., Gammie, P., Sewell, T., Winwood, S.: Provable security: How feasible is it? In: 13th HotOS, Napa, CA, USA, pp. 28\u201332. USENIX (May 2011)"},{"key":"23_CR6","unstructured":"Leino, K.R.M., Yessenov, K.: Stepwise refinement of heap-manipulating code in Chalice (2011) Unpublished manuscript, \n                    \n                      http:\/\/research.microsoft.com\/en-us\/um\/people\/leino\/papers\/krml211.pdf"},{"issue":"4","key":"23_CR7","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1145\/942572.807045","volume":"9","author":"B. Liskov","year":"1974","unstructured":"Liskov, B., Zilles, S.: Programming with abstract data types. SIGPLAN Not.\u00a09(4), 50\u201359 (1974)","journal-title":"SIGPLAN Not."},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"Murray, T., Lowe, G.: On refinement-closed security properties and nondeterministic compositions. In: 8th AVoCS, Glasgow, UK. ENTCS, vol.\u00a0250, pp. 49\u201368 (2009)","DOI":"10.1016\/j.entcs.2009.08.017"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-642-22863-6_24","volume-title":"Interactive Theorem Proving","author":"T. Sewell","year":"2011","unstructured":"Sewell, T., Winwood, S., Gammie, P., Murray, T., Andronick, J., Klein, G.: seL4 Enforces Integrity. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 325\u2013340. Springer, Heidelberg (2011)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-642-10373-5_24","volume-title":"Formal Methods and Software Engineering","author":"R. Silva","year":"2009","unstructured":"Silva, R., Butler, M.: Supporting Reuse of Event-B Developments through Generic Instantiation. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol.\u00a05885, pp. 466\u2013484. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33826-7_23.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:22:14Z","timestamp":1620130934000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33826-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642338250","9783642338267"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33826-7_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}