{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:13:17Z","timestamp":1774987997753,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540878728","type":"print"},{"value":"9783540878735","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-87873-5_8","type":"book-chapter","created":{"date-parts":[[2008,9,25]],"date-time":"2008-09-25T08:04:10Z","timestamp":1222329850000},"page":"54-69","source":"Crossref","is-referenced-by-count":22,"title":["Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems"],"prefix":"10.1007","author":[{"given":"Xinyu","family":"Feng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yu","family":"Guo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuan","family":"Dong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"11","key":"8_CR1","doi-asserted-by":"publisher","first-page":"1382","DOI":"10.1109\/32.41331","volume":"15","author":"W.R. Bevier","year":"1989","unstructured":"Bevier, W.R.: Kit: A study in operating system verification. IEEE Trans. Softw. Eng.\u00a015(11), 1382\u20131396 (1989)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"4","key":"8_CR2","first-page":"409","volume":"5","author":"W.R. Bevier","year":"1989","unstructured":"Bevier, W.R., Hunt, W.A., Moore, J.S., Young, W.D.: Special issue on system verification. Journal of Automated Reasoning\u00a05(4), 409\u2013530 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"Cai, H., Shao, Z., Vaynberg, A.: Certified self-modifying code. In: PLDI 2007, pp. 66\u201377 (June 2007)","DOI":"10.1145\/1250734.1250743"},{"key":"8_CR4","unstructured":"Coq Development Team. The Coq proof assistant reference manual. The Coq release v8.1"},{"key":"8_CR5","unstructured":"Elphinstone, K., Klein, G., Derrin, P., Roscoe, T., Heiser, G.: Towards a practical, verified kernel. In: Proc. 11th Workshop on Hot Topics in Operating Systems (May 2007)"},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"Feng, X., Ni, Z., Shao, Z., Guo, Y.: An open framework for foundational proof-carrying code. In: TLDI 2007, pp. 67\u201378 (January 2007)","DOI":"10.1145\/1190315.1190325"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z., Dong, Y., Guo, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. In: PLDI 2008 ( to appear, June 2008)","DOI":"10.1145\/1375581.1375603"},{"key":"8_CR8","unstructured":"Feng, X., Shao, Z., Guo, Y., Dong, Y.: Combining domain-specific and foundational logics to verify complete software systems, extended version and Coq implementations (2008), http:\/\/flint.cs.yale.edu\/flint\/publications\/itrimp.html"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z., Vaynberg, A., Xiang, S., Ni, Z.: Modular verification of assembly code with stack-based control abstractions. In: PLDI 2006, pp. 401\u2013414 (June 2006)","DOI":"10.1145\/1133981.1134028"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Gargano","year":"2005","unstructured":"Gargano, M., Hillebrand, M.A., Leinenbach, D., Paul, W.J.: On the correctness of operating system kernels. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603. Springer, Heidelberg (2005)"},{"issue":"4","key":"8_CR11","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. on Programming Languages and Systems\u00a05(4), 596\u2013619 (1983)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"McCreight, A., Shao, Z., Lin, C., Li, L.: A general framework for certifying garbage collectors and their mutators. In: PLDI 2007, pp. 468\u2013479 (June 2007)","DOI":"10.1145\/1250734.1250788"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: Proc. 33rd ACM Symp. on Principles of Prog. Lang, pp. 320\u2013333 (2006)","DOI":"10.1145\/1111037.1111066"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/978-3-540-74591-4_15","volume-title":"Theorem Proving in Higher Order Logics","author":"Z. Ni","year":"2007","unstructured":"Ni, Z., Yu, D., Shao, Z.: Using XCAP to certify realistic systems code: Machine context management. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 189\u2013206. Springer, Heidelberg (2007)"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-540-28644-8_4","volume-title":"CONCUR 2004 - Concurrency Theory","author":"P.W. O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 49\u201367. Springer, Heidelberg (2004)"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL 2004, pp. 268\u2013280 (January 2004)","DOI":"10.1145\/982962.964024"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037116","volume-title":"Typed Lambda Calculi and Applications","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C.: Inductive definitions in the system Coq\u2014rules and properties. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol.\u00a0664. Springer, Heidelberg (1993)"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proc. LICS 2002, pp. 55\u201374 (July 2002)","DOI":"10.1109\/LICS.2002.1029817"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-87873-5_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:50:48Z","timestamp":1619509848000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-87873-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540878728","9783540878735"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-87873-5_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}