{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T20:15:47Z","timestamp":1784232947930,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540745907","type":"print"},{"value":"9783540745914","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74591-4_15","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T14:49:52Z","timestamp":1187794192000},"page":"189-206","source":"Crossref","is-referenced-by-count":22,"title":["Using XCAP to Certify Realistic Systems Code: Machine Context Management"],"prefix":"10.1007","author":[{"given":"Zhaozhong","family":"Ni","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dachuan","family":"Yu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"15_CR1","volume-title":"Proc. 34th ACM Symp. on Principles of Prog. Lang.","author":"A.W. Appel","year":"2007","unstructured":"Appel, A.W., Mellies, P.-A., Richards, C.D., Vouillon, J.: A very modal model of a modern, major, general type system. In: Proc. 34th ACM Symp. on Principles of Prog. Lang., January 2007, ACM Press, New York (2007)"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Feng, X., Ni, Z., Shao, Z., Guo, Y.: An open framework for foundational proof-carrying code. In: Proc. Workshop on Types in Language Design and Implementation (January 2007)","DOI":"10.1145\/1190315.1190325"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","first-page":"2","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Gargano","year":"2005","unstructured":"Gargano, M., Hillebrand, M., Leinenbach, D., Paul, W.: On the correctness of operating system kernels. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 2\u201316. Springer, Heidelberg (2005)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM (October 1969)","DOI":"10.1145\/363235.363259"},{"key":"15_CR5","unstructured":"Hunt, G.C., Larus, J.R., Abadi, M., Aiken, M., Barham, P., Fahndrich, M., Hawblitzel, C., Hodson, O., Levi, S., Murphy, N., Steensgaard, B., Tarditi, D., Wobber, T., Zill, B.: An overview of the Singularity project. Technical Report MSR-TR-2005-135, Microsoft Research, Redmond, WA (October 2005)"},{"key":"15_CR6","first-page":"14","volume-title":"Proc. 28th ACM Symp. on Principles of Prog. Lang.","author":"S.S. Ishtiaq","year":"2001","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proc. 28th ACM Symp. on Principles of Prog. Lang., pp. 14\u201326. ACM Press, New York (2001)"},{"key":"15_CR7","unstructured":"Jabber software development list: Jabberd crash in swapcontext() via _mio_raw_connect() (2001), http:\/\/mailman.jabber.org\/pipermail\/jdev\/2001-March\/005655.html"},{"key":"15_CR8","unstructured":"Libc for alpha systems mailing list: {make,set,swap}context broken on powerpc32 (2006), http:\/\/www.archivesat.com\/Libc_for_alpha_systems\/thread2267226.htm"},{"key":"15_CR9","first-page":"85","volume-title":"Proc. 25th ACM Symp. on Principles of Prog. Lang.","author":"G. Morrisett","year":"1998","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. In: Proc. 25th ACM Symp. on Principles of Prog. Lang., January 1998, pp. 85\u201397. ACM Press, New York (1998)"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Myreen, M.O., Gordon, M.J.C.: Hoare logic for realistically modelled machine code. In: Proc. 13th International Conference on Tools and Algorithms for Construction and Analysis of Systems (2007)","DOI":"10.1007\/978-3-540-71209-1_44"},{"key":"15_CR11","unstructured":"NetBSD port-amd64 mailing list: swapcontext(3) does not work? (2004), http:\/\/mail-index.netbsd.org\/port-amd64\/2004\/11\/30\/0003.html"},{"key":"15_CR12","volume-title":"Proc. 33rd ACM Symp. on Principles of Prog. Lang.","author":"Z. Ni","year":"2006","unstructured":"Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: Proc. 33rd ACM Symp. on Principles of Prog. Lang., January 2006, ACM Press, New York (2006)"},{"key":"15_CR13","unstructured":"Ni, Z., Shao, Z.: A translation from typed assembly languages to certified assembly programming (October 2006), flint.cs.yale.edu\/flint\/publications\/talcap.html"},{"key":"15_CR14","unstructured":"Ni, Z., Yu, D., Shao, Z.: Coq code for using xcap to certify realistic systems code: Machine context management (March 2007), http:\/\/flint.cs.yale.edu\/flint\/publications\/mctx.html"},{"key":"15_CR15","unstructured":"Ni, Z., Yu, D., Shao, Z.: Technical report for using xcap to certify realistic systems code: machine context management (June 2007), http:\/\/flint.cs.yale.edu\/flint\/publications\/mctx.html"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Proc. 17th Symp. on Logic in Computer Science (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"15_CR17","unstructured":"SecurityTracker.com: Solaris 10 x64 kernel setcontext() bug lets local users deny service (2006), http:\/\/securitytracker.com\/alerts\/2006\/Feb\/1015557.html"},{"key":"15_CR18","unstructured":"The Coq Development Team: The Coq proof assistant reference manual (v8.0) (2004)"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"The glibc-bugs mailing list: [bug libc\/357] new: getcontext() on ppc32 destroys saved parameter 1 in caller\u2019s frame (2004), http:\/\/sourceware.org\/ml\/glibc-bugs\/2004-08\/msg00201.html","DOI":"10.1016\/S1353-4858(04)00085-6"},{"key":"15_CR20","unstructured":"The glibc-bugs mailing list: [bug libc\/612] new: makecontext broken on powerpc-linux (2004), http:\/\/sources.redhat.com\/ml\/glibc-bugs\/2004-12\/msg00102.html"},{"key":"15_CR21","unstructured":"Yu, Y.: Automated Proofs of Object Code For A Widely Used Microprocessor. PhD thesis, The University of Texas at Austin (1992)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74591-4_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T21:38:20Z","timestamp":1684013900000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74591-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745907","9783540745914"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74591-4_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}