{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:18:16Z","timestamp":1725455896890},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642351815"},{"type":"electronic","value":"9783642351822"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-35182-2_23","type":"book-chapter","created":{"date-parts":[[2012,12,6]],"date-time":"2012-12-06T01:19:15Z","timestamp":1354756755000},"page":"315-331","source":"Crossref","is-referenced-by-count":5,"title":["Modular Verification of Concurrent Thread Management"],"prefix":"10.1007","author":[{"given":"Yu","family":"Guo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xinyu","family":"Feng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peizhi","family":"Shi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"23_CR1","first-page":"20","volume-title":"Proc. of ATEC 2000","author":"R.S. Engelschall","year":"2000","unstructured":"Engelschall, R.S.: Portable multithreading: the signal stack trick for user-space thread creation. In: Proc. of ATEC 2000, p. 20. USENIX Association, Berkeley (2000)"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Engler, D.R., Kaashoek, M.F., O\u2019Toole Jr., J.: Exokernel: an operating system architecture for application-level resource management. In: Proceedings of the 15th ACM Symposium on Operating Systems Principles, SOSP 1995, Copper Mountain Resort, Colorado, pp. 251\u2013266 (December 1995)","DOI":"10.1145\/224056.224076"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-540-87873-5_8","volume-title":"Verified Software: Theories, Tools, Experiments","author":"X. Feng","year":"2008","unstructured":"Feng, X., Shao, Z., Guo, Y., Dong, Y.: Combining Domain-Specific and Foundational Logics to Verify Complete Software Systems. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 54\u201369. Springer, Heidelberg (2008)"},{"key":"23_CR4","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: Proc. PLDI 2006, pp. 401\u2013414 (June 2006)","DOI":"10.1145\/1133981.1134028"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11541868_1","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.F. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 1\u201316. Springer, Heidelberg (2005)"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"Gotsman, A., Yang, H.: Modular verification of preemptive os kernels. In: Proc. ICFP 2011, Tokyo, Japan, pp. 404\u2013417. ACM (2011)","DOI":"10.1145\/2034574.2034827"},{"key":"23_CR7","doi-asserted-by":"crossref","unstructured":"Guo, Y., Feng, X., Shao, Z., Shi, P.: Modular verification of concurrent thread management (technical report and coq proof) (June 2012), \n                    \n                      http:\/\/kyhcs.ustcsz.edu.cn\/~guoyu\/sched\/","DOI":"10.1007\/978-3-642-35182-2_23"},{"key":"23_CR8","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1145\/1151374.1151391","volume":"40","author":"J.N. Herder","year":"2006","unstructured":"Herder, J.N., Bos, H., Gras, B., Homburg, P., Tanenbaum, A.S.: Minix 3: a highly reliable, self-repairing operating system. SIGOPS Oper. Syst. Rev.\u00a040, 80\u201389 (2006)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"23_CR9","unstructured":"Hohmuth, M., Tews, H.: The vfiasco approach for a verified operating system. In: Proceedings of the 2nd ECOOP Workshop on Programming Languages and Operating Systems (2005)"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"In der Rieden, T., Tsyban, A.: CVM \u2013 A verified framework for microkernel programmers. In: Proc. SSV 2008. Electronic Notes in Theoretical Computer Science, vol.\u00a0217C, pp. 151\u2013168. Elsevier Science B.V. (2008)","DOI":"10.1016\/j.entcs.2008.06.047"},{"key":"23_CR11","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: Proc. SOSP 2009, Big Sky, MT, USA, pp. 207\u2013220. ACM (October 2009)","DOI":"10.1145\/1629575.1629596"},{"key":"23_CR12","unstructured":"Love, R.: Linux Kernel Development, 2nd edn. Novell Press (2005)"},{"key":"23_CR13","unstructured":"McKusick, M.K., Neville-Neil, G.V.: The Design and Implementation of the FreeBSD Operating System. Pearson Education (2004)"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: Proc. POPL 2006, pp. 320\u2013333 (January 2006)","DOI":"10.1145\/1111320.1111066"},{"key":"23_CR15","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)"},{"issue":"1-3","key":"23_CR16","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P.W. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theor. Comput. Sci.\u00a0375(1-3), 271\u2013307 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR17","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/LICS.2002.1029817","volume-title":"LICS 2002: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pp. 55\u201374. IEEE Computer Society, Washington, DC (2002)"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-540-87873-5_20","volume-title":"Verified Software: Theories, Tools, Experiments","author":"A. Starostin","year":"2008","unstructured":"Starostin, A., Tsyban, A.: Verified Process-Context Switch for C-Programmed Kernels. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 240\u2013254. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35182-2_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,9]],"date-time":"2019-05-09T18:51:34Z","timestamp":1557427894000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35182-2_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642351815","9783642351822"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35182-2_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}