{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T23:04:03Z","timestamp":1784675043550,"version":"3.55.0"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319415390","type":"print"},{"value":"9783319415406","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41540-6_4","type":"book-chapter","created":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T09:34:07Z","timestamp":1468316047000},"page":"59-79","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":56,"title":["A Practical Verification Framework for Preemptive OS Kernels"],"prefix":"10.1007","author":[{"given":"Fengwei","family":"Xu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ming","family":"Fu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xinyu","family":"Feng","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xiaoran","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hui","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhaohui","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,7,13]]},"reference":[{"key":"4_CR1","unstructured":"The coq development team: The Coq proof assistant. \n                      http:\/\/coq.inria.fr"},{"key":"4_CR2","unstructured":"The real-time kernel: $$\\mu $$C\/OS-II. \n                      http:\/\/micrium.com\/rtos\/ucosii\/overview"},{"key":"4_CR3","unstructured":"The Verisoft XT Project (2007). \n                      http:\/\/www.verisoftxt.de"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-15057-9_5","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E Alkassar","year":"2010","unstructured":"Alkassar, E., Paul, W.J., Starostin, A., Tsyban, A.: Pervasive verification of an OS microkernel. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol. 6217, pp. 71\u201385. Springer, Heidelberg (2010)"},{"key":"4_CR5","unstructured":"Appel, A.W.: Tactics for separation logic (2006). \n                      http:\/\/www.cs.princeton.edu\/~appel\/papers\/septacs.pdf"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/BF01088832","volume":"5","author":"O Babaoglu","year":"1993","unstructured":"Babaoglu, O., Marzullo, K., Schneider, F.B.: A formalization of priority inversion. Real-Time Syst. 5, 285\u2013303 (1993)","journal-title":"Real-Time Syst."},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Cao, J., Fu, M., Feng, X.: Practical tactics for verifying C programs in coq. In: CPP, pp. 97\u2013108 (2015)","DOI":"10.1145\/2676724.2693162"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Chen, H., Wu, N., Shao, Z., Lockerman, J., Gu, R.: Toward compositional verification of interruptible os kernels and device drivers. In: PLDI (2016, to appear)","DOI":"10.1145\/2908080.2908101"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"4_CR11","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, pp. 170\u2013182 (2008)","DOI":"10.1145\/1379022.1375603"},{"issue":"4","key":"4_CR12","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1017\/S0956796813000075","volume":"23","author":"A Gotsman","year":"2013","unstructured":"Gotsman, A., Yang, H.: Modular verification of preemptive OS kernels. J. Funct. Program. 23(4), 452\u2013514 (2013)","journal-title":"J. Funct. Program."},{"issue":"1","key":"4_CR13","doi-asserted-by":"crossref","first-page":"595","DOI":"10.1145\/2775051.2676975","volume":"50","author":"Ronghui Gu","year":"2015","unstructured":"Gu, R., Koenig, J., Ramananandro, T., Shao, Z., Wu, X.N., Weng, S.-C., Zhang, H., Guo, Y.: Deep specifications and certified abstraction layers. In: POPL, pp. 595\u2013608 (2015)","journal-title":"ACM SIGPLAN Notices"},{"issue":"6","key":"4_CR14","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an operating-system kernel. Commun. ACM 53(6), 107\u2013115 (2010)","journal-title":"Commun. ACM"},{"issue":"1","key":"4_CR15","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/2560537","volume":"32","author":"G Klein","year":"2014","unstructured":"Klein, G., Andronick, J., Elphinstone, K., Murray, T.C., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32(1), 2 (2014)","journal-title":"ACM Trans. Comput. Syst."},{"key":"4_CR16","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 (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X.: Modular verification of linearizability with non-fixed linearization points. In: PLDI, pp. 459\u2013470 (2013)","DOI":"10.1145\/2499370.2462189"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X., Fu, M.: A rely-guarantee-based simulation for verifying concurrent program transformations. In: POPL, pp. 455\u2013468 (2012)","DOI":"10.1145\/2103621.2103711"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Liang, H., Feng, X., Shao, Z.: Compositional verification of termination-preserving refinement of concurrent programs. In: CSL-LICS, pp. 65: 1\u201365: 10 (2014)","DOI":"10.1145\/2603088.2603123"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-642-03359-9_24","volume-title":"Theorem Proving in Higher Order Logics","author":"A McCreight","year":"2009","unstructured":"McCreight, A.: Practical tactics for separation logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 343\u2013358. Springer, Heidelberg (2009)"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-28644-8_4","volume-title":"CONCUR 2004 - Concurrency Theory","author":"PW O\u2019Hearn","year":"2004","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 49\u201367. Springer, Heidelberg (2004)"},{"issue":"3","key":"4_CR22","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/2487241.2487248","volume":"60","author":"J Sevc\u00edk","year":"2013","unstructured":"Sevc\u00edk, J., Vafeiadis, V., Nardelli, F.Z., Jagannathan, S., Sewell, P.: Compcerttso: a verified compiler for relaxed-memory concurrency. J. ACM 60(3), 22 (2013)","journal-title":"J. ACM"},{"key":"4_CR23","doi-asserted-by":"publisher","first-page":"1175","DOI":"10.1109\/12.57058","volume":"39","author":"L Sha","year":"1990","unstructured":"Sha, L., Rajkumar, R., Lehoczky, J.P.: Priority inheritance protocols: an approach to real-time synchronization. IEEE Trans. Comput. 39, 1175\u20131185 (1990)","journal-title":"IEEE Trans. Comput."},{"key":"4_CR24","doi-asserted-by":"crossref","unstructured":"Turon, A., Dreyer, D., Birkedal, L.: Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In: ICFP, pp. 377\u2013390 (2013)","DOI":"10.1145\/2544174.2500600"},{"issue":"1","key":"4_CR25","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1145\/2480359.2429111","volume":"48","author":"Aaron J. Turon","year":"2013","unstructured":"Turon, A., Thamsborg, J., Ahmed, A., Birkedal, L., Dreyer, D.: Logical relations for fine-grained concurrency. In: POPL, pp. 343\u2013356 (2013)","journal-title":"ACM SIGPLAN Notices"},{"key":"4_CR26","doi-asserted-by":"crossref","unstructured":"Xu, F., Fu, M., Feng, X., Zhang, X., Zhang, H., Li, Z.: A practical verification framework for preemptive OS kernels (technical report and coq implementations), May 2016. \n                      http:\/\/staff.ustc.edu.cn\/~fuming\/research\/certiucos","DOI":"10.1007\/978-3-319-41540-6_4"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: PLDI, pp. 99\u2013110 (2010)","DOI":"10.1145\/1809028.1806610"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41540-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:07:11Z","timestamp":1594685231000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41540-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415390","9783319415406"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41540-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 July 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}