{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:10:14Z","timestamp":1755997814488},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642288906"},{"type":"electronic","value":"9783642288913"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28891-3_21","type":"book-chapter","created":{"date-parts":[[2012,3,30]],"date-time":"2012-03-30T08:53:01Z","timestamp":1333097581000},"page":"210-215","source":"Crossref","is-referenced-by-count":10,"title":["Sound Formal Verification of Linux\u2019s USB BP Keyboard Driver"],"prefix":"10.1007","author":[{"given":"Willem","family":"Penninckx","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan Tobias","family":"M\u00fchlberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Smans","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bart","family":"Jacobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank","family":"Piessens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"21_CR1","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":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-540-73368-3_22","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2007","unstructured":"Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P., Wies, T., Yang, H.: Shape Analysis for Composite Data Structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 178\u2013192. Springer, Heidelberg (2007)"},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"Bornat, R., Calcagno, C., O\u2019Hearn, P., Parkinson, M.: Permission accouting in separation logic. In: POPL (2005)","DOI":"10.1145\/1040305.1040327"},{"key":"21_CR4","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/502034.502042","volume-title":"SOSP 2001","author":"A. Chou","year":"2001","unstructured":"Chou, A., Yang, J., Chelf, B., Hallem, S., Engler, D.R.: An empirical study of operating system errors. In: SOSP 2001, pp. 73\u201388. ACM, New York (2001)"},{"issue":"5","key":"21_CR5","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"21_CR6","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.\u00a05674, pp. 23\u201342. Springer, Heidelberg (2009)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-76637-7_3","volume-title":"Programming Languages and Systems","author":"A. Gotsman","year":"2007","unstructured":"Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local Reasoning for Storable Locks and Threads. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol.\u00a04807, pp. 19\u201337. Springer, Heidelberg (2007)"},{"key":"21_CR8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/1278901.1278904","volume":"41","author":"G. Heiser","year":"2007","unstructured":"Heiser, G., Elphinstone, K., Kuz, I., Klein, G., Petters, S.M.: Towards trustworthy computing systems: taking microkernels to the next level. SIGOPS Oper. Syst. Rev.\u00a041, 3\u201311 (2007)","journal-title":"SIGOPS Oper. Syst. Rev."},{"key":"21_CR9","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":"10","key":"21_CR10","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013580 and 583 (1969)","journal-title":"Communications of the ACM"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B. Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 41\u201355. Springer, Heidelberg (2011)"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/978-3-642-10452-7_17","volume-title":"Formal Methods: Foundations and Applications","author":"M. Kim","year":"2009","unstructured":"Kim, M., Kim, Y.: Concolic Testing of the Multi-sector Read Operation for Flash Memory File System. In: Oliveira, M.V.M., Woodcock, J. (eds.) SBMF 2009. LNCS, vol.\u00a05902, pp. 251\u2013265. Springer, Heidelberg (2009)"},{"key":"21_CR13","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 and PDMC 2006. LNCS, vol.\u00a04346, pp. 211\u2013226. Springer, Heidelberg (2007)"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-10452-7_21","volume-title":"Formal Methods: Foundations and Applications","author":"J.T. M\u00fchlberg","year":"2009","unstructured":"M\u00fchlberg, J.T., L\u00fcttgen, G.: Verifying Compiled File System Code. In: Oliveira, M.V.M., Woodcock, J. (eds.) SBMF 2009. LNCS, vol.\u00a05902, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"key":"21_CR15","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1002\/stvr.399","volume":"19","author":"H. Post","year":"2009","unstructured":"Post, H., Sinz, C., K\u00fcchlin, W.: Towards automatic software model checking of thousands of Linux modules \u2013 a case study with Avinux. Softw. Test. Verif. Reliab.\u00a019, 155\u2013172 (2009)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"21_CR16","first-page":"55","volume-title":"LICS 2002","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, pp. 55\u201374. IEEE, Washington (2002)"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-642-21461-5_21","volume-title":"Formal Techniques for Distributed Systems","author":"F. Vogels","year":"2011","unstructured":"Vogels, F., Jacobs, B., Piessens, F., Smans, J.: Annotation Inference for Separation Logic Based Verifiers. In: Bruni, R., Dingel, J. (eds.) FMOODS\/FORTE 2011. LNCS, vol.\u00a06722, pp. 319\u2013333. Springer, Heidelberg (2011)"},{"key":"21_CR18","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1145\/1321631.1321719","volume-title":"ASE 2007","author":"T. Witkowski","year":"2007","unstructured":"Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent Linux device drivers. In: ASE 2007, pp. 501\u2013504. ACM, New York (2007)"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-70545-1_36","volume-title":"Computer Aided Verification","author":"H. Yang","year":"2008","unstructured":"Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O\u2019Hearn, P.: Scalable Shape Analysis for Systems Code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 385\u2013398. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28891-3_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T22:03:14Z","timestamp":1606168994000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28891-3_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288906","9783642288913"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28891-3_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}