{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T10:07:46Z","timestamp":1743156466132,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319192482"},{"type":"electronic","value":"9783319192499"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-19249-9_18","type":"book-chapter","created":{"date-parts":[[2015,5,23]],"date-time":"2015-05-23T07:55:31Z","timestamp":1432367731000},"page":"273-290","source":"Crossref","is-referenced-by-count":2,"title":["Automated Verification of RPC Stub Code"],"prefix":"10.1007","author":[{"given":"Matthew","family":"Fernandez","sequence":"first","affiliation":[]},{"given":"June","family":"Andronick","sequence":"additional","affiliation":[]},{"given":"Gerwin","family":"Klein","sequence":"additional","affiliation":[]},{"given":"Ihor","family":"Kuz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"crossref","unstructured":"Adamek, J.: Static analysis of component systems using behavior protocols. In: OOPSLA, Anaheim, CA, US, pp. 116\u2013117 (October 2003)","DOI":"10.1145\/949344.949378"},{"issue":"3","key":"18_CR2","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/MS.2011.27","volume":"28","author":"A. Basu","year":"2011","unstructured":"Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.H., Sifakis, J.: Rigorous component-based system design using the BIP framework. Softw.\u00a028(3), 41\u201348 (2011)","journal-title":"Softw."},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-41202-8_6","volume-title":"Formal Methods and Software Engineering","author":"A. Boyton","year":"2013","unstructured":"Boyton, A., et al.: Formally verified system initialisation. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol.\u00a08144, pp. 70\u201385. Springer, Heidelberg (2013)"},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.M. Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., P\u0103s\u0103reanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 331\u2013346. Springer, Heidelberg (2003)"},{"key":"18_CR5","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":"18_CR6","doi-asserted-by":"crossref","unstructured":"Fernandez, M., Kuz, I., Klein, G., Andronick, J.: Towards a verified component platform. In: PLOS, Farmington, PA, USA, p. 6 (November 2013)","DOI":"10.1145\/2525528.2525535"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-540-69149-5_10","volume-title":"Verified Software: Theories, Tools, Experiments","author":"K. Fisler","year":"2008","unstructured":"Fisler, K., Adsul, B.: Decomposing verification around end-user features. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol.\u00a04171, pp. 74\u201381. Springer, Heidelberg (2008)"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Giannakopoulou, D., P\u0103s\u0103reanu, C.S., Barringer, H.: Assumption generation for software component verification. In: 17th ASE, Edinburgh, UK, pp. 3\u201312 (September 2002)","DOI":"10.1109\/ASE.2002.1114984"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Edinburgh LCF","year":"1979","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P. (eds.): Edinburgh LCF. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-642-32347-8_8","volume-title":"Interactive Theorem Proving","author":"D. Greenaway","year":"2012","unstructured":"Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: Automatic verified abstraction of C. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 99\u2013115. Springer, Heidelberg (2012)"},{"key":"18_CR11","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: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, Edinburgh, UK, pp. 429\u2013439 (June 2014)","DOI":"10.1145\/2594291.2594296"},{"key":"18_CR12","unstructured":"ISO\/IEC: Programming languages \u2014 C. Technical Report 9899:TC2, ISO\/IEC JTC1\/SC22\/WG14 (May 2005)"},{"key":"18_CR13","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, Big Sky, MT, USA, pp. 207\u2013220 (October 2009)","DOI":"10.1145\/1629575.1629596"},{"issue":"5","key":"18_CR14","first-page":"687","volume":"80","author":"I. Kuz","year":"2007","unstructured":"Kuz, I., Liu, Y., Gorton, I., Heiser, G.: CAmkES: A component model for secure microkernel-based embedded systems. Journal of Systems and Software Special Edition on Component-Based Software Engineering of Trustworthy Embedded Systems\u00a080(5), 687\u2013699 (2007)","journal-title":"Journal of Systems and Software Special Edition on Component-Based Software Engineering of Trustworthy Embedded Systems"},{"key":"18_CR15","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: Programming a compiler with a proof assistant. In: 33rd POPL, Charleston, SC, USA, pp. 42\u201354 (2006)","DOI":"10.1145\/1111037.1111042"},{"issue":"4","key":"18_CR16","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. JAR\u00a043(4), 363\u2013446 (2009)","journal-title":"JAR"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Murray, T., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., Klein, G.: seL4: from general purpose to a proof of information flow enforcement. In: IEEE Symp. Security & Privacy, San Francisco, CA, pp. 415\u2013429 (May 2013)","DOI":"10.1109\/SP.2013.35"},{"key":"18_CR18","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Lee, P.: Safe kernel extensions without run-time checking. In: 2nd OSDI, Seattle, WA, US, pp. 229\u2013243 (October 1996)","DOI":"10.1145\/248155.238781"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M.D., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"key":"18_CR21","doi-asserted-by":"crossref","unstructured":"Ramananandro, T., Shao, Z., Weng, S.C., Koenig, J., Fu, Y.: A compositional semantics for verified separate compilation and linking. In: 4th CPP, Mumbai, India, pp. 3\u201314 (January 2015)","DOI":"10.1145\/2676724.2693167"},{"key":"18_CR22","unstructured":"Reynolds, J.C.: Separation logic: A logic for mutable data structures, Copenhagen, Denmark (July 2002)"},{"key":"18_CR23","doi-asserted-by":"crossref","unstructured":"Schirmer, N.: Verification of Sequential Imperative Programs in Isabelle\/HOL. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Sewell, T., Myreen, M., Klein, G.: Translation validation for a verified OS kernel. In: PLDI, Seattle, Washington, USA, pp. 471\u2013481 (June 2013)","DOI":"10.1145\/2499370.2462183"},{"key":"18_CR25","unstructured":"Szyperski, C.: Component Software: Beyond Object-Oriented Programming, Essex, England (1997)"},{"key":"18_CR26","unstructured":"Trustworthy Systems Team: seL4 v1.03 (August 2014) (release August 10, 2014)"},{"key":"18_CR27","doi-asserted-by":"crossref","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: 34th POPL, Nice, France, pp. 97\u2013108 (January 2007)","DOI":"10.1145\/1190216.1190234"},{"key":"18_CR28","unstructured":"Wenzel, M.: The Isabelle\/Isar Reference Manual (August 2014)"},{"key":"18_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/978-3-642-03359-9_34","volume-title":"Theorem Proving in Higher Order Logics","author":"S. Winwood","year":"2009","unstructured":"Winwood, S., Klein, G., Sewell, T., Andronick, J., Cock, D., Norrish, M.: Mind the gap: A verification framework for low-level C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 500\u2013515. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","FM 2015: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-19249-9_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,9]],"date-time":"2024-06-09T05:35:38Z","timestamp":1717911338000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-19249-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319192482","9783319192499"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-19249-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}