{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:53:12Z","timestamp":1725511992018},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540709510"},{"type":"electronic","value":"9783540709527"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-70952-7_14","type":"book-chapter","created":{"date-parts":[[2007,6,26]],"date-time":"2007-06-26T08:40:01Z","timestamp":1182847201000},"page":"211-226","source":"Crossref","is-referenced-by-count":15,"title":["Blasting Linux Code"],"prefix":"10.1007","author":[{"given":"Jan Tobias","family":"M\u00fchlberg","sequence":"first","affiliation":[]},{"given":"Gerald","family":"L\u00fcttgen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) Model Checking Software. LNCS, vol.\u00a02057, pp. 103\u2013122. Springer, Heidelberg (2001)"},{"key":"14_CR2","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/1014007.1014028","volume-title":"PEPM 2004","author":"D. Beyer","year":"2004","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: The BLAST query language for software verification. In: PEPM 2004, pp. 201\u2013202. ACM Press, New York (2004)"},{"key":"14_CR3","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)"},{"unstructured":"Breuer, P.T., Pickin, S.: Abstract interpretation meets model checking near the 10<Superscript>6<\/Superscript> LOC mark. In: AVIS 2006, To appear in ENTCS","key":"14_CR4"},{"issue":"2\u20133","key":"14_CR5","first-page":"129","volume":"25","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E., Groce, A., Ouaknine, J., Strichman, O., Yorav, K.: Efficient verification of sequential and concurrent C programs. FMSD\u00a025(2\u20133), 129\u2013166 (2004)","journal-title":"FMSD"},{"key":"14_CR6","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 Press, New York (2001)"},{"key":"14_CR7","volume-title":"Model checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press, Cambridge (2000)"},{"key":"14_CR8","volume-title":"Linux Device Drivers","author":"J. Corbet","year":"2005","unstructured":"Corbet, J., Rubini, A., Kroah-Hartmann, G.: Linux Device Drivers, 3rd edn. O\u2019Reilly, Sebastopol (2005)","edition":"3"},{"doi-asserted-by":"crossref","unstructured":"Corbett, J.C., et al.: Bandera: Extracting finite-state models from Java source code. In: ICST 2000, pp. 439\u2013448. SQS Publishing (2000)","key":"14_CR9","DOI":"10.1145\/337180.337234"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/3-540-45657-0_3","volume-title":"Computer Aided Verification","author":"P. Cousot","year":"2002","unstructured":"Cousot, P., Cousot, R.: On abstraction in software verification. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 37\u201356. Springer, Heidelberg (2002)"},{"doi-asserted-by":"crossref","unstructured":"Engler, D.R., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. In: OSDI 2000, USENIX (2000)","key":"14_CR11","DOI":"10.21236\/ADA419626"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/978-3-540-24622-0_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D.R. Engler","year":"2004","unstructured":"Engler, D.R., Musuvathi, M.: Static analysis versus software model checking for bug finding. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 191\u2013210. Springer, Heidelberg (2004)"},{"key":"14_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/996841.996844","volume-title":"PLDI 2004","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: PLDI 2004, pp. 1\u201313. ACM Press, New York (2004)"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","first-page":"232","volume-title":"Verification: Theory and Practice","author":"T.A. Henzinger","year":"2004","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sanvido, M.A.A.: Extreme model cecking. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol.\u00a02772, pp. 232\u2013358. Springer, Heidelberg (2004)"},{"key":"14_CR15","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/503272.503279","volume-title":"POPL 2002","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002, pp. 58\u201370. ACM Press, New York (2002)"},{"key":"14_CR16","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., et al.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 526\u2013538. Springer, Heidelberg (2002)"},{"key":"14_CR17","volume-title":"The SPIN model checker","author":"G.J. Holzmann","year":"2003","unstructured":"Holzmann, G.J.: The SPIN model checker. Addison-Wesley, Reading (2003)"},{"unstructured":"Jie, H., Shivaji, S.: Temporal safety verification of AVFS using BLAST. Project report, Univ. California at Santa Cruz (2004)","key":"14_CR18"},{"unstructured":"Microsoft Corporation. Static driver verifier: Finding bugs in device drivers at compile-time. http:\/\/www.microsoft.com\/whdc\/devtools\/tools\/SDV.mspx","key":"14_CR19"},{"unstructured":"Mong, W.S.: Lazy abstraction on software model checking. Project report, Toronto Univ., Canada (2004)","key":"14_CR20"},{"key":"14_CR21","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1145\/503272.503286","volume-title":"POPL 2002","author":"G.C. Necula","year":"2002","unstructured":"Necula, G.C., McPeaki, S., Weimer, W.: CCured: Type-safe retrofitting of legacy code. In: POPL 2002, pp. 128\u2013139. ACM Press, New York (2002)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Applications and Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70952-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T16:34:44Z","timestamp":1556555684000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70952-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540709510","9783540709527"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70952-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}