{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T09:20:57Z","timestamp":1762507257754,"version":"3.37.3"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2017,12,23]],"date-time":"2017-12-23T00:00:00Z","timestamp":1513987200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,12,23]],"date-time":"2017-12-23T00:00:00Z","timestamp":1513987200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["1319671","1521523"],"award-info":[{"award-number":["1319671","1521523"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000144","name":"Division of Computer and Network Systems","doi-asserted-by":"publisher","award":["1065451"],"award-info":[{"award-number":["1065451"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-12-2-0293","FA8750-15-C-0082"],"award-info":[{"award-number":["FA8750-12-2-0293","FA8750-15-C-0082"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004543","name":"China Scholarship Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100004543","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10817-017-9446-0","type":"journal-article","created":{"date-parts":[[2017,12,23]],"date-time":"2017-12-23T15:54:02Z","timestamp":1514044442000},"page":"141-189","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Toward Compositional Verification of Interruptible OS Kernels and Device Drivers"],"prefix":"10.1007","volume":"61","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1180-9433","authenticated-orcid":false,"given":"Hao","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiongnan","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joshua","family":"Lockerman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ronghui","family":"Gu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,12,23]]},"reference":[{"key":"9446_CR1","doi-asserted-by":"crossref","unstructured":"Alkassar, E.: OS verication extended: on the formal verication of device drivers and the correctness of client\/server software. PhD thesis, Saarland University, Computer Science Department (2009)","DOI":"10.1007\/s12046-009-0004-2"},{"key":"9446_CR2","doi-asserted-by":"crossref","unstructured":"Alkassar, E., Hillebrand, M.A.: Formal functional verification of device drivers. In: Proceedings of the Verified Software: Theories, Tools, Experiments Second International Conference (VSTTE), Toronto, Canada, pp. 225\u2013239 (2008)","DOI":"10.1007\/978-3-540-87873-5_19"},{"key":"9446_CR3","unstructured":"Alkassar, E., Cohen, E., Hillebrand, M., Pentchev, H.: Modular specification and verification of interprocess communication. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, FMCAD Inc, Austin, TX, FMCAD \u201910, pp. 167\u2013174 (2010a)"},{"key":"9446_CR4","doi-asserted-by":"crossref","unstructured":"Alkassar, E., Paul, W., Starostin, A., Tsyban, A.: Pervasive verification of an OS microkernel: inline assembly, memory consumption, concurrent devices. In: Verified Software: Theories, Tools, Experiments (VSTTE 2010), Edinburgh, UK, pp. 71\u201385 (2010b)","DOI":"10.1007\/978-3-642-15057-9_5"},{"key":"9446_CR5","doi-asserted-by":"crossref","unstructured":"Amani, S., Chubb, P., Donaldson, A., Legg, A., Ryzhyk, L., Zhu, Y.: Automatic verification of message-based device drivers. In: Systems Software Verification, Sydney, Australia, pp. 1\u201314 (2012)","DOI":"10.4204\/EPTCS.102.3"},{"key":"9446_CR6","doi-asserted-by":"crossref","unstructured":"Andronick, J., Lewis, C., Morgan, C.: Controlled Owicki-Gries concurrency: reasoning about the preemptible eChronos embedded operating system. In: van Glabbeek RJ, Groote JF, H\u00f6fner P (eds) Workshop on models for formal analysis of real systems (MARS 2015), Suva, Fiji, pp. 10\u201324 (2015)","DOI":"10.4204\/EPTCS.196.2"},{"key":"9446_CR7","first-page":"52","volume-title":"Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency","author":"J Andronick","year":"2016","unstructured":"Andronick, J., Lewis, C., Matichuk, D., Morgan, C., Rizkallah, C.: Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency, pp. 52\u201368. Springer, Berlin (2016)"},{"key":"9446_CR8","doi-asserted-by":"crossref","unstructured":"Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: Proceedings of the 1st ACM SIGOPS\/EuroSys European Conference on Computer Systems 2006, ACM, New York, NY, USA, EuroSys \u201906, pp. 73\u201385 (2006)","DOI":"10.1145\/1217935.1217943"},{"key":"9446_CR9","unstructured":"Ball, T., Bounimova, E., Kumar, R., Levin, V.: SLAM2: Static driver verification with under 4% false alarms. In: Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design, FMCAD Inc, Austin, TX, FMCAD \u201910, pp. 35\u201342 (2010)"},{"issue":"3","key":"9446_CR10","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10817-009-9148-3","volume":"43","author":"S Blazy","year":"2009","unstructured":"Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reason. 43(3), 263\u2013288 (2009)","journal-title":"J. Autom. Reason."},{"key":"9446_CR11","doi-asserted-by":"crossref","unstructured":"Chen, H., Wu, X.N., Shao, Z., Lockerman, J., Gu, R.: Toward compositional verification of interruptible OS kernels and device drivers. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, New York, NY, USA, PLDI \u201916, pp. 431\u2013447 (2016)","DOI":"10.1145\/2980983.2908101"},{"key":"9446_CR12","doi-asserted-by":"crossref","unstructured":"Chou, A., Yang, J., Chelf, B., Hallem, S., Engler, D.: An empirical study of operating systems errors. In: Proceedings of the 18th ACM Symposium on Operating Systems Principles, ACM, New York, NY, USA, SOSP \u201901, pp. 73\u201388 (2001)","DOI":"10.1145\/502034.502042"},{"key":"9446_CR13","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201908), pp. 337\u2013340 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9446_CR14","unstructured":"Duan, J.: Formal verification of device drivers in embedded systems. PhD thesis, University of Utah (2013)"},{"key":"9446_CR15","unstructured":"Duan, J., Regehr, J.: Correctness proofs for device drivers in embedded systems. In: Proceedings of the 5th International Conference on Systems Software Verification, USENIX Association, Berkeley, CA, USA, SSV\u201910, p. 5 (2010)"},{"key":"9446_CR16","doi-asserted-by":"crossref","unstructured":"Feng, X., Shao, Z., Dong, Y., Guo, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. In: Proceedings of the ACM Conference on Programming Language Design and Implementation, pp. 170\u2013182 (2008)","DOI":"10.1145\/1379022.1375603"},{"issue":"2\u20134","key":"9446_CR17","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/s10817-009-9118-9","volume":"42","author":"X Feng","year":"2009","unstructured":"Feng, X., Shao, Z., Guo, Y., Dong, Y.: Certifying low-level programs with hardware interrupts and preemptive threads. J. Autom. Reason. 42(2\u20134), 301\u2013347 (2009)","journal-title":"J. Autom. Reason."},{"key":"9446_CR18","unstructured":"Ganapathi, A., Ganapathi, V., Patterson, D.: Windows XP kernel crash analysis. In: Proceedings of the 20th Conference on Large Installation System Administration, USENIX Association, Berkeley, CA, USA, LISA \u201906, pp. 12\u201312 (2006)"},{"key":"9446_CR19","doi-asserted-by":"crossref","unstructured":"Gu, R., Koenig, J., Ramananandro, T., Shao, Z., Wu, X., Weng, S.C., Zhang, H., Guo, Y.: Deep specifications and certified abstraction layers. In: Proceedings of the 42nd ACM Symposium on Principles of Programming Languages, pp. 595\u2013608 (2015)","DOI":"10.1145\/2775051.2676975"},{"key":"9446_CR20","unstructured":"Gu, R., Shao, Z., Chen, H., Wu, X.N., Kim, J., Sj\u00f6berg, V., Costanzo, D.: Certikos: An extensible architecture for building certified concurrent os kernels. In: Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation, USENIX Association, Berkeley, CA, USA, OSDI\u201916, pp. 653\u2013669 (2016)"},{"key":"9446_CR21","unstructured":"Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad apps: end-to-end security via automated full-system verification. In: Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation (2014)"},{"key":"9446_CR22","unstructured":"Intel: 82093AA I\/O advanced programmable interrupt controller (I\/O APIC) datasheet. Specification (1996)"},{"key":"9446_CR23","unstructured":"Intel: Multiprocessor specification, version 1.4. Specification (1997)"},{"key":"9446_CR24","doi-asserted-by":"crossref","unstructured":"Khoroshilov, A., Mutilin, V., Petrenko, A., Zakharov, V.: Establishing Linux driver verification process. In: Pnueli, A., Virbitskaite, I., Voronkov, A. (eds.) Perspectives of Systems Informatics. Lecture Notes in Computer Science, vol. 5947, pp. 165\u2013176. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-11486-1_14"},{"key":"9446_CR25","doi-asserted-by":"crossref","unstructured":"Kim, M., Choi, Y., Kim, Y., Kim, H.: Formal verification of a flash memory device driver - an experience report. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) Model Checking Software. Lecture Notes in Computer Science, vol. 5156, pp. 144\u2013159. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-85114-1_12"},{"key":"9446_CR26","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: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP), Big Sky, MT, US, pp. 207\u2013220 (2009)","DOI":"10.1145\/1629575.1629596"},{"issue":"1","key":"9446_CR27","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., 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":"9446_CR28","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Proceedings of the Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2010), pp. 348\u2013370 (2010)","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"9446_CR29","unstructured":"Leroy, X.: The CompCert verified compiler. \n                    http:\/\/compcert.inria.fr\/\n                    \n                   (2005\u20132013)"},{"issue":"1","key":"9446_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformation. J. Autom. Reason. 41(1), 1\u201331 (2008)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9446_CR31","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"NA Lynch","year":"1995","unstructured":"Lynch, N.A., Vaandrager, F.W.: Forward and backward simulations: I. Untimed systems. Inf. Comput. 121(2), 214\u2013233 (1995)","journal-title":"Inf. Comput."},{"key":"9446_CR32","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: Verification of device drivers and intelligent controllers: a case study. In: Kirsch C, Wilhelm, R. (eds.) Proceedings of the 7th ACM International Conference On Embedded Software, EMSOFT 2007, pp. 30\u201336. ACM & IEEE (2007)","DOI":"10.1145\/1289927.1289937"},{"key":"9446_CR33","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. In: Proceedings of the 15th International Conference on Concurrency Theory (CONCUR\u201904), pp. 49\u201367 (2004)","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"9446_CR34","unstructured":"Paul, W., Broy, M., In der Rieden, T.: The Verisoft XT Project. \n                    http:\/\/www.verisoft.de\n                    \n                   (2007)"},{"key":"9446_CR35","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, vol. 828. Springer (1994)","DOI":"10.1007\/BFb0030541"},{"key":"9446_CR36","unstructured":"Pentchev, H.: Sound semantics of a high-level language with interprocessor interrupts. PhD thesis, Saarland University, Computer Science Department (2016)"},{"key":"9446_CR37","doi-asserted-by":"crossref","unstructured":"Ryzhyk, L., Chubb, P., Kuz, I., Le\u00a0Sueur, E., Heiser, G.: Automatic device driver synthesis with Termite. In: Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles (SOSP), Big Sky, MT, US, pp. 73\u201386 (2009)","DOI":"10.1145\/1629575.1629583"},{"key":"9446_CR38","unstructured":"Ryzhyk, L., Walker, A.C., Keys, J., Legg, A., Raghunath, A., Stumm, M., Vij, M.: User-guided device driver synthesis. In: USENIX Symposium on Operating Systems Design and Implementation, Broomfield, CO, USA, pp. 661\u2013676 (2014)"},{"key":"9446_CR39","doi-asserted-by":"crossref","unstructured":"Schwarz, O., Dam, M.: Formal verification of secure user mode device execution with DMA. In: Yahav, E. (ed.) Hardware and Software: Verification and Testing, Lecture Notes in Computer Science, vol. 8855, pp. 236\u2013251. Springer (2014)","DOI":"10.1007\/978-3-319-13338-6_18"},{"key":"9446_CR40","unstructured":"The Coq development team: The Coq proof assistant. \n                    http:\/\/coq.inria.fr\n                    \n                   (1999\u20132016)"},{"key":"9446_CR41","unstructured":"Witkowski, T.: Formal verification of Linux device drivers. Master\u2019s thesis, Dresden University of Technology (2007)"},{"key":"9446_CR42","doi-asserted-by":"crossref","unstructured":"Yang, J., Hawblitzel, C.: Safe to the last instruction: automated verification of a type-safe operating system. In: Proceedings of the 2010 ACM Conference on Programming Language Design and Implementation, pp. 99\u2013110 (2010)","DOI":"10.1145\/1809028.1806610"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9446-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9446-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9446-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,13]],"date-time":"2020-05-13T23:01:51Z","timestamp":1589410911000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9446-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,23]]},"references-count":42,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["9446"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9446-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2017,12,23]]},"assertion":[{"value":"1 April 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 December 2017","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 December 2017","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}