{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T15:00:46Z","timestamp":1791039646114,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540732099","type":"print"},{"value":"9783540732105","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73210-5_27","type":"book-chapter","created":{"date-parts":[[2007,9,13]],"date-time":"2007-09-13T04:03:05Z","timestamp":1189656185000},"page":"518-537","source":"Crossref","is-referenced-by-count":17,"title":["Integrated Static Analysis for Linux Device Driver Verification"],"prefix":"10.1007","author":[{"given":"Hendrik","family":"Post","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wolfgang","family":"K\u00fcchlin","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"27_CR1","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1145\/945445.945466","volume-title":"19th ACM Symp. on Operating Systems Principles, Proc.","author":"M.M. Swift","year":"2003","unstructured":"Swift, M.M., Bershad, B.N., Levy, H.M.: Improving the reliability of commodity operating systems. In: 19th ACM Symp. on Operating Systems Principles, Proc., pp. 207\u2013222. ACM Press, New York (2003)"},{"issue":"4","key":"27_CR2","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. ACM SIGOPS Oper. Syst. Rev.\u00a040(4), 73\u201385 (2006)","journal-title":"ACM SIGOPS Oper. Syst. Rev."},{"key":"27_CR3","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":"27_CR4","unstructured":"Ball, T., Rajamani, S.K.: SLIC: A specification language for interface checking. Technical report, Microsoft Research (2001)"},{"key":"27_CR5","unstructured":"Various: The SLAM Project (2006), http:\/\/research.microsoft.com\/slam\/"},{"key":"27_CR6","unstructured":"Post, H., Sinz, C., K\u00fcchlin, W.: Avinux: Towards automatic verification of Linux device drivers (2007), Available at http:\/\/www-sr.informatik.uni-tuebingen.de\/~post\/avinux"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with blast. In: Ball, T., Rajamani, S.K. (eds.) Model Checking Software. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"27_CR8","first-page":"439","volume-title":"Software Engineering, 22nd Intl. Conf., Proc.","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Robby, Z.H.: Bandera: extracting finite-state models from Java source code. In: Software Engineering, 22nd Intl. Conf., Proc., pp. 439\u2013448. ACM Press, New York (2000)"},{"key":"27_CR9","unstructured":"Various: Linux kernel releases (Available online under http:\/\/www.kernel.org )"},{"key":"27_CR10","unstructured":"Corbet, J., Rubini, A., Kroah-Hartman, G.: Linux Device Drivers, 3rd edn. O\u2019Reilly Media, Inc. (2005)"},{"key":"27_CR11","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1145\/996841.996845","volume-title":"ACM SIGPLAN Conf. on Programming Language Design and Implementation, Proc.","author":"S. Qadeer","year":"2004","unstructured":"Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: ACM SIGPLAN Conf. on Programming Language Design and Implementation, Proc., vol.\u00a039, pp. 14\u201324. ACM Press, New York (2004)"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. pp. 82\u201397","DOI":"10.1007\/11513988_9"},{"issue":"2","key":"27_CR13","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1145\/356586.356588","volume":"3","author":"E.G. Coffman","year":"1971","unstructured":"Coffman, E.G., Elphick, M., Shoshani, A.: System deadlocks. ACM Comput. Surv.\u00a03(2), 67\u201378 (1971)","journal-title":"ACM Comput. Surv."},{"key":"27_CR14","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., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol.\u00a04346, pp. 211\u2013226. Springer, Heidelberg (2007)"},{"key":"27_CR15","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/1181195.1181215","volume-title":"Conf. on Specification and verification of component-based systems, Proc.","author":"H. Post","year":"2006","unstructured":"Post, H., K\u00fcchlin, W.: Automatic data environment construction for static device drivers analysis. In: Conf. on Specification and verification of component-based systems, Proc., pp. 89\u201392. ACM Press, New York (2006)"},{"issue":"4","key":"27_CR16","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1145\/1189256.1189259","volume":"24","author":"J. Yang","year":"2006","unstructured":"Yang, J., Twohey, P., Engler, D., Musuvathi, M.: Using model checking to find serious file system errors. ACM Trans. Comput. Syst.\u00a024(4), 393\u2013423 (2006)","journal-title":"ACM Trans. Comput. Syst."},{"key":"27_CR17","first-page":"263","volume-title":"ESEC\/SIGSOFT FSE","author":"K. Sen","year":"2005","unstructured":"Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for c. In: Wermelinger, M., Gall, H. (eds.) ESEC\/SIGSOFT FSE, pp. 263\u2013272. ACM Press, New York (2005)"},{"key":"27_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G.C. Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: Cil: Intermediate language and tools for analysis and transformation of c programs. In: Horspool, R.N. (ed.) CC 2002 and ETAPS 2002. LNCS, vol.\u00a02304, pp. 213\u2013228. Springer, Heidelberg (2002)"},{"key":"27_CR19","unstructured":"Sauter, M.: Automatisierung und Integration regelbasierter Verifikation f\u00fcr Linux Ger\u00e4tetreiber. Master\u2019s Thesis (to appear, 2007)"},{"key":"27_CR20","first-page":"385","volume-title":"Software Engineering","author":"S. Chaki","year":"2003","unstructured":"Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: Software Engineering. 25th Intl. Conf., Proc, pp. 385\u2013395. IEEE Computer Society, Washington, DC (2003)"},{"key":"27_CR21","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1145\/586110.586142","volume-title":"ACM Intl. Conf. on Computer and Communications Security, Proc.","author":"H. Chen","year":"2002","unstructured":"Chen, H., Wagner, D.: MOPS: an infrastructure for examining security properties of software. In: Atluri, V. (ed.) ACM Intl. Conf. on Computer and Communications Security, Proc., pp. 235\u2013244. ACM, New York (2002)"},{"issue":"2","key":"27_CR22","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1145\/234528.234740","volume":"28","author":"P. Cousot","year":"1996","unstructured":"Cousot, P.: Abstract interpretation. ACM Comput. Surv.\u00a028(2), 324\u2013328 (1996)","journal-title":"ACM Comput. Surv."},{"key":"27_CR23","doi-asserted-by":"crossref","unstructured":"Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: Software verification platform. [33], pp. 301\u2013306","DOI":"10.1007\/11513988_31"},{"key":"27_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/11817963_17","volume-title":"Computer Aided Verification","author":"N. Sethi","year":"2006","unstructured":"Sethi, N., Barrett, C.: Cascade: C assertion checker and deductive engine. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 166\u2013169. Springer, Heidelberg (2006)"},{"key":"27_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/11691372_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Chaki","year":"2006","unstructured":"Chaki, S., Clarke, E.M., Kidd, N., Reps, T.W., Touili, T.: Verifying concurrent message-passing C programs with recursive calls. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 334\u2013349. Springer, Heidelberg (2006)"},{"key":"27_CR26","first-page":"55","volume-title":"LICS","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55\u201374. IEEE Computer Society, Los Alamitos (2002)"},{"key":"27_CR27","unstructured":"Various: Linux standard base project, (Available online under http:\/\/www.linuxbase.org )"},{"key":"27_CR28","unstructured":"Various: The OLVER project, (Available under http:\/\/linuxtesting.org )"},{"key":"27_CR29","unstructured":"Chen, H., Dean, D., Wagner, D.: Model checking one million lines of C code. In: NDSS, The Internet Society (2004)"},{"key":"27_CR30","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1145\/945445.945468","volume-title":"19th ACM Symp. on Operating Systems Principles, Proc.","author":"D. Engler","year":"2003","unstructured":"Engler, D., Ashcraft, K.: RacerX: effective, static detection of race conditions and deadlocks. In: 19th ACM Symp. on Operating Systems Principles, Proc., pp. 237\u2013252. ACM Press, New York (2003)"},{"key":"27_CR31","first-page":"351","volume-title":"32nd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, Proc.","author":"Y. Xie","year":"2005","unstructured":"Xie, Y., Aiken, A.: Scalable error detection using boolean satisfiability. In: 32nd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, Proc., pp. 351\u2013363. ACM Press, New York (2005)"},{"key":"27_CR32","unstructured":"Meissner, F.: Regelbasierte Spezifikation von Linux Kernel-Schnittstellen mit SLIC. Master\u2019s Thesis (to appear, 2007)"},{"key":"27_CR33","series-title":"Lecture Notes in Computer Science","first-page":"6","volume-title":"Computer Aided Verification","year":"2005","unstructured":"Etessami, K., Rajamani, S.K. (eds.): CAV 2005. LNCS, vol.\u00a03576, pp. 6\u201310. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73210-5_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,23]],"date-time":"2021-08-23T09:42:48Z","timestamp":1629711768000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73210-5_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540732099","9783540732105"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73210-5_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}