{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T20:54:46Z","timestamp":1777582486032,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642114854","type":"print"},{"value":"9783642114861","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11486-1_14","type":"book-chapter","created":{"date-parts":[[2010,1,27]],"date-time":"2010-01-27T08:39:51Z","timestamp":1264581591000},"page":"165-176","source":"Crossref","is-referenced-by-count":35,"title":["Establishing Linux Driver Verification Process"],"prefix":"10.1007","author":[{"given":"Alexey","family":"Khoroshilov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vadim","family":"Mutilin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Petrenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vladimir","family":"Zakharov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","unstructured":"Gillen, A., Stergiades, E., Waldman, B.: The role of Linux servers and commercial workloads (2008), http:\/\/www.linux-foundation.org\/publications\/IDC_Workloads.pdf"},{"key":"14_CR2","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/502034.502042","volume-title":"SOSP 2001: Proceedings of the eighteenth ACM symposium on Operating systems principles","author":"A. Chou","year":"2001","unstructured":"Chou, A., Yang, J., Chelf, B., Hallem, S., Engler, D.: An empirical study of operating systems errors. In: SOSP 2001: Proceedings of the eighteenth ACM symposium on Operating systems principles, pp. 73\u201388. ACM, New York (2001)"},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/945445.945466","volume-title":"SOSP 2003: Proceedings of the nineteenth ACM symposium on Operating systems principles","author":"M.M. Swift","year":"2003","unstructured":"Swift, M.M., Bershad, B.N., Levy, H.M.: Improving the reliability of commodity operating systems. In: SOSP 2003: Proceedings of the nineteenth ACM symposium on Operating systems principles, pp. 207\u2013222. ACM, New York (2003)"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Senyard, A., Michlmayr, M.: How to have a successful free software project. In: 11th Asia-Pacific Software Engineering Conference, pp. 84\u201391 (2004)","DOI":"10.1109\/APSEC.2004.58"},{"key":"14_CR5","unstructured":"Kroah-Hartman, G., Corbet, J., McPherson, A.: Linux kernel development (2008), http:\/\/www.linux-foundation.org\/publications\/linuxkerneldevelopment.php"},{"key":"14_CR6","unstructured":"Kroah-Hartman, G.: The Linux kernel driver interface, http:\/\/www.kernel.org\/doc\/Documentation\/stable_api_nonsense.txt"},{"key":"14_CR7","volume-title":"The Cathedral and the Bazaar: Musings on Linux and Open Source by an Accidental Revolutionary","author":"E.S. Raymond","year":"2001","unstructured":"Raymond, E.S.: The Cathedral and the Bazaar: Musings on Linux and Open Source by an Accidental Revolutionary. O\u2019Reilly, Sebastopol (2001)"},{"key":"14_CR8","volume-title":"Facts and Fallacies of Software Engineering","author":"R.L. Glass","year":"2003","unstructured":"Glass, R.L.: Facts and Fallacies of Software Engineering, 1st edn. Addison Wesley Professional, Sebastopol (2003)","edition":"1"},{"key":"14_CR9","unstructured":"Web-site: Linux Verification Center, http:\/\/linuxtesting.ru"},{"key":"14_CR10","unstructured":"LKML: Message 41536, http:\/\/www.mail-archive.com\/git-commits-head@vger.kernel.org\/msg41536.html"},{"key":"14_CR11","unstructured":"Ball, T., Rajamani, S.K.: SLIC: A specification language for interface checking. Technical report, Microsoft Research (2001)"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"518","DOI":"10.1007\/978-3-540-73210-5_27","volume-title":"Integrated Formal Methods","author":"H. Post","year":"2007","unstructured":"Post, H., K\u00fcchlin, W.: Integrated static analysis for Linux device driver verification. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol.\u00a04591, pp. 518\u2013537. Springer, Heidelberg (2007)"},{"issue":"1","key":"14_CR13","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1145\/982962.964021","volume":"39","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. SIGPLAN Not.\u00a039(1), 232\u2013244 (2004)","journal-title":"SIGPLAN Not."},{"key":"14_CR14","first-page":"58","volume-title":"Symposium on Principles of Programming Languages","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Lazy abstraction. In: Symposium on Principles of Programming Languages, pp. 58\u201370. ACM Press, New York (2002)"},{"issue":"4","key":"14_CR15","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/1218063.1217943","volume":"40","author":"T. Ball","year":"2006","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. SIGOPS Oper. Syst. Rev.\u00a040(4), 73\u201385 (2006)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: technology transfer of formal methods inside Microsoft. Technical report, Microsoft Research (2004)","DOI":"10.1007\/978-3-540-24756-2_1"},{"key":"14_CR17","unstructured":"Breuer, P., Pickin, S.: Open source certification. FLOSS-FM (2008)"},{"issue":"5","key":"14_CR18","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1145\/381694.378846","volume":"36","author":"T. Ball","year":"2001","unstructured":"Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. SIGPLAN Not.\u00a036(5), 203\u2013213 (2001)","journal-title":"SIGPLAN Not."},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 526\u2013538. Springer, Heidelberg (2002)"},{"issue":"5","key":"14_CR20","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","volume":"9","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: The software model checker Blast: Applications to software engineering. Int. J. Softw. Tools Technol. Transf.\u00a09(5), 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/978-3-540-31984-9_2","volume-title":"Fundamental Approaches to Software Engineering","author":"D. Beyer","year":"2005","unstructured":"Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: Checking memory safety with blast. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol.\u00a03442, pp. 2\u201318. Springer, Heidelberg (2005)"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-540-70952-7_14","volume-title":"Formal Methods: Applications and Technology","author":"J.T. M\u00fchlberg","year":"2007","unstructured":"M\u00fchlberg, J.T., L\u00fcttgen, G.: Blasting Linux code. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol.\u00a04346, pp. 211\u2013226. Springer, Heidelberg (2007)"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"14_CR24","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1145\/1321631.1321719","volume-title":"ASE 2007: Proceedings of the twenty-second IEEE\/ACM international conference on Automated software engineering","author":"T. Witkowski","year":"2007","unstructured":"Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent Linux device drivers. In: ASE 2007: Proceedings of the twenty-second IEEE\/ACM international conference on Automated software engineering, pp. 501\u2013504. ACM, New York (2007)"},{"key":"14_CR25","unstructured":"Witkowski, T.: Formal verification of Linux device drivers. Master\u2019s thesis, Dresden University of Technology (2007)"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Breuer, P., Pickin, S.: Verification in the light and large: Large-scale verification for fast-moving open source C projects. In: Software Engineering Workshop, Annual IEEE\/NASA Goddard, pp. 246\u2013255 (2007)","DOI":"10.1109\/SEW.2007.37"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Kim, M., Hong, S., Hong, C., Kim, T.: Model-based kernel tesiting for concurrency bugs through counter example replay. In: Fifth Workshop on Model-Based Testing (2009)","DOI":"10.1016\/j.entcs.2009.09.049"},{"key":"14_CR28","unstructured":"Coverity: Linux report (2004), http:\/\/scan.coverity.com"}],"container-title":["Lecture Notes in Computer Science","Perspectives of Systems Informatics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11486-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,17]],"date-time":"2025-02-17T00:23:59Z","timestamp":1739751839000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11486-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642114854","9783642114861"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11486-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}