{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T17:18:57Z","timestamp":1742923137384,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662468227"},{"type":"electronic","value":"9783662468234"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46823-4_32","type":"book-chapter","created":{"date-parts":[[2015,4,18]],"date-time":"2015-04-18T01:40:54Z","timestamp":1429321254000},"page":"400-414","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Modeling Environment for Static Verification of Linux Kernel Modules"],"prefix":"10.1007","author":[{"given":"Alexey","family":"Khoroshilov","sequence":"first","affiliation":[]},{"given":"Vadim","family":"Mutilin","sequence":"additional","affiliation":[]},{"given":"Evgeny","family":"Novikov","sequence":"additional","affiliation":[]},{"given":"Ilja","family":"Zakharov","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,19]]},"reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"Palix, N., Thomas, G., Saha, S., Calv\u00e8s, C., Lawall, J., Muller, G.: Faults in Linux: ten years later. In: Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS XVI, pp. 305\u2013318. ACM (2011)","DOI":"10.1145\/1961296.1950401"},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"Mutilin, V., Novikov, E., Khoroshilov, A.: Analysis of typical faults in Linux operating system drivers (in Russian). In: Proceedings of the Institute for System Programming of RAS, vol. 22, pp. 349\u2013374 (2012)","DOI":"10.15514\/ISPRAS-2012-22-19"},{"key":"32_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011)"},{"issue":"5\u20136","key":"32_CR4","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., Jhala, R., Majumdar, R.: The software model checker BLAST. Int. J. Softw. Tools Technol. Transfer. 9(5\u20136), 505\u2013525 (2007)","journal-title":"Int. J. Softw. Tools Technol. Transfer."},{"key":"32_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/978-3-642-28756-5_39","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Shved","year":"2012","unstructured":"Shved, P., Mandrykin, M., Mutilin, V.: Predicate analysis with BLAST 2.7. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 525\u2013527. Springer, Heidelberg (2012)"},{"key":"32_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"32_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/978-3-642-36742-7_52","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Albarghouthi","year":"2013","unstructured":"Albarghouthi, A., Gurfinkel, A., Li, Y., Chaki, S., Chechik, M.: UFO: verification with interpolants and abstract interpretation. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 637\u2013640. Springer, Heidelberg (2013)"},{"key":"32_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-540-24622-0_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D Engler","year":"2004","unstructured":"Engler, D., Musuvathi, M.: Static analysis versus software model checking for bug finding. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 191\u2013210. Springer, Heidelberg (2004)"},{"issue":"1","key":"32_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","volume":"100","author":"R Milner","year":"1992","unstructured":"Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, I. Inf. Comput. 100(1), 1\u201340 (1992)","journal-title":"Inf. Comput."},{"key":"32_CR10","unstructured":"Milner, R.: The Polyadic $$\\pi $$-Calculus: a Tutorial. Department of Computer Science, University of Edinburgh, LFCS (1991)"},{"key":"32_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-29709-0_17","volume-title":"Perspectives of Systems Informatics","author":"A Khoroshilov","year":"2012","unstructured":"Khoroshilov, A., Mutilin, V., Novikov, E., Shved, P., Strakh, A.: Towards an open framework for C verification tools benchmarking. In: Clarke, E., Virbitskaite, I., Voronkov, A. (eds.) PSI 2011. LNCS, vol. 7162, pp. 179\u2013192. Springer, Heidelberg (2012)"},{"key":"32_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"594","DOI":"10.1007\/978-3-642-36742-7_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2013","unstructured":"Beyer, D.: Second competition on software verification. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 594\u2013609. Springer, Heidelberg (2013)"},{"issue":"4","key":"32_CR13","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1134\/S0361768813040051","volume":"39","author":"E Novikov","year":"2013","unstructured":"Novikov, E.: An approach to implementation of aspect-oriented programming for C. Program. Comput. Softw. 39(4), 194\u2013206 (2013)","journal-title":"Program. Comput. Softw."},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"Zakharov, I., Mutilin, V., Novikov, E., Khoroshilov, A.: Environment modeling of Linux operating system device drivers (in Russian). In: Proceedings of the Institute for System Programming of RAS, vol. 25, pp. 85\u2013112 (2013)","DOI":"10.15514\/ISPRAS-2013-25-6"},{"key":"32_CR15","doi-asserted-by":"crossref","unstructured":"Witkowski, T., Blanc, N., Kroening, D., Weissenbacher, G.: Model checking concurrent Linux device drivers. In: Proceedings of the 22nd IEEE\/ACM International Conference on Automated Software Engineering, pp. 501\u2013504. ACM, New York (2007)","DOI":"10.1145\/1321631.1321719"},{"key":"32_CR16","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. 4591, pp. 518\u2013537. Springer, Heidelberg (2007)"},{"issue":"4","key":"32_CR17","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. 40(4), 73\u201385 (2006)","journal-title":"SIGOPS Oper. Syst. Rev."}],"container-title":["Lecture Notes in Computer Science","Perspectives of System Informatics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46823-4_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,21]],"date-time":"2023-02-21T00:41:59Z","timestamp":1676940119000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-46823-4_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662468227","9783662468234"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46823-4_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"19 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}