{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:32:45Z","timestamp":1774837965785,"version":"3.50.1"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319431437","type":"print"},{"value":"9783319431444","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-43144-4_20","type":"book-chapter","created":{"date-parts":[[2016,8,6]],"date-time":"2016-08-06T04:24:16Z","timestamp":1470457456000},"page":"323-340","source":"Crossref","is-referenced-by-count":15,"title":["A Framework for the Automatic Formal Verification of Refinement from Cogent to C"],"prefix":"10.1007","author":[{"given":"Christine","family":"Rizkallah","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Japheth","family":"Lim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yutaka","family":"Nagashima","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Sewell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zilin","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Liam","family":"O\u2019Connor","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Toby","family":"Murray","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gabriele","family":"Keller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,8,7]]},"reference":[{"key":"20_CR1","unstructured":"Cogent material (2016). https:\/\/github.com\/NICTA\/cogent\/tree\/itp_2016"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Amani, S., Hixon, A., Chen, Z., Rizkallah, C., Chubb, P., O\u2019Connor, L., Beeren, J., Nagashima, Y., Lim, J., Sewell, T., Tuong, J., Keller, G., Murray, T., Klein, G., Heiser, G.: Cogent: Verifying high-assurance file system implementations. In: ASPLOS, pp. 175\u2013188, April 2016","DOI":"10.1145\/2954679.2872404"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 5170, pp. 167\u2013182. Springer, Heidelberg (2008)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Greenaway, D., Lim, J., Andronick, J., Klein, G.: Don\u2019t sweat the small stuff: formal verification of C code without the pain. In: PLDI, pp. 429\u2013439 (June 2014)","DOI":"10.1145\/2666356.2594296"},{"key":"20_CR5","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: SOSP, pp. 207\u2013220 (October 2009)","DOI":"10.1145\/1629575.1629596"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: POPL, pp. 179\u2013191, January 2014","DOI":"10.1145\/2535838.2535841"},{"issue":"7","key":"20_CR7","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. CACM 52(7), 107\u2013115 (2009)","journal-title":"CACM"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"20_CR9","unstructured":"O\u2019Connor, L., Chen, Z., Rizkallah, C., Amani, S., Lim, J., Murray, T., Nagashima, Y., Sewell, T., Klein, G.: Refinement through restraint: bringing down the cost of verification. In: ICFP (to appear, 2016)"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. SIGPLAN Lisp Pointers V(1), 288\u2013298 (January 1992)","DOI":"10.1145\/141478.141563"},{"key":"20_CR11","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle\/HOL. Ph.D. thesis, Technische Universit\u00e4t M\u00fcnchen (2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Sewell, T., Myreen, M., Klein, G.: Translation validation for a verified OS kernel. In: PLDI, pp. 471\u2013481 (June 2013)","DOI":"10.1145\/2491956.2462183"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: POPL, pp. 97\u2013108 (January 2007)","DOI":"10.1145\/1190216.1190234"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-43144-4_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,12]],"date-time":"2019-09-12T07:37:32Z","timestamp":1568273852000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-43144-4_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319431437","9783319431444"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-43144-4_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}