{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,10]],"date-time":"2026-11-10T23:40:32Z","timestamp":1794354032912,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540787990","type":"print"},{"value":"9783540788003","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78800-3_10","type":"book-chapter","created":{"date-parts":[[2008,4,2]],"date-time":"2008-04-02T04:26:19Z","timestamp":1207110379000},"page":"124-140","source":"Crossref","is-referenced-by-count":15,"title":["Analyzing Stripped Device-Driver Executables"],"prefix":"10.1007","author":[{"given":"Gogul","family":"Balakrishnan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"http:\/\/www.microsoft.com\/whdc\/devtools\/ddk\/default.mspx"},{"key":"10_CR2","unstructured":"Defrauding the WHQL driver certification process, March (2004), http:\/\/blogs.msdn.com\/oldnewthing\/archive\/2004\/03\/05\/84469.aspx"},{"key":"10_CR3","unstructured":"C++ for kernel mode drivers: Pros and cons, WHDC web site (February 2007), http:\/\/www.microsoft.com\/whdc\/driver\/kernel\/KMcode.mspx"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G.: WYSINWYX: What You See Is Not What You eXecute. PhD thesis, C.S. Dept. Univ. of Wisconsin, Madison, WI, August, TR-1603 (2007)","DOI":"10.1007\/978-3-540-69149-5_22"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/978-3-540-24723-4_2","volume-title":"Compiler Construction","author":"G. Balakrishnan","year":"2004","unstructured":"Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In: Duesterwald, E. (ed.) CC 2004. LNCS, vol.\u00a02985, pp. 5\u201323. Springer, Heidelberg (2004)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-540-71322-7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T. Reps","year":"2007","unstructured":"Reps, T., Balakrishnan, G.: DIVINE: DIscovering Variables IN Executables. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 1\u201328. Springer, Heidelberg (2007)"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","first-page":"158","volume-title":"Computer Aided Verification","author":"T. Reps","year":"2005","unstructured":"Reps, T., Melski, D., Lal, A.K., Teitelbaum, T., Balakrishnan, G., Gruian, R., Kidd, N., Lim, J., Yong, S., Chen, C.-H.: Model checking x86 executables with CodeSurfer\/x86 and WPDS++. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 158\u2013163. Springer, Heidelberg (2005)"},{"key":"10_CR8","unstructured":"Balakrishnan, G., Reps, T., Melski, D., Teitelbaum, T.: WYSINWYX: What You See Is Not What You eXecute. In: IFIP Working Conf. on VSTTE (2005)"},{"key":"10_CR9","unstructured":"Ball, T.: Personal communication (February 2006)"},{"key":"10_CR10","doi-asserted-by":"crossref","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. In: EuroSys. (2006)","DOI":"10.1145\/1217935.1217943"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for Boolean programs. In: Spin Workshop (2000)","DOI":"10.1007\/10722468_7"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S.K. Rajamani","year":"2001","unstructured":"Rajamani, S.K., Ball, T.: The SLAM Toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, Springer, Heidelberg (2001)"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI (2003)","DOI":"10.1145\/781131.781153"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, Springer, Heidelberg (1997)"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Chou, A., Yang, J., Chelf, B., Hallem, S., Engler, D.: An empirical study of operating systems errors. In: SOSP (2001)","DOI":"10.21236\/ADA419594"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL (1979)","DOI":"10.1145\/567752.567778"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: PLDI (2002)","DOI":"10.1145\/512529.512538"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/11823230_1","volume-title":"Static Analysis","author":"M. Das","year":"2006","unstructured":"Das, M., Yang, Y., Dhurjati, D.: Path-Sensitive Dataflow Analysis with Iterative Refinement. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 425\u2013442. Springer, Heidelberg (2006)"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Elec. Notes in Theor. Comp. Sci.\u00a09 (1997)","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/11594116","volume-title":"Fast Software Encryption","author":"J. Fischer","year":"2005","unstructured":"Fischer, J., Jhala, R., Majumdar, R.: Joining dataflow with predicates. In: Gilbert, H., Handschuh, H. (eds.) FSE 2005. LNCS, vol.\u00a03557, Springer, Heidelberg (2005)"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, Springer, Heidelberg (1997)"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)","DOI":"10.1145\/503272.503279"},{"issue":"1","key":"10_CR23","first-page":"60","volume":"7","author":"L.H. Holley","year":"1981","unstructured":"Holley, L.H., Rosen, B.K.: Qualified data flow problems. TSE\u00a07(1), 60\u201378 (1981)","journal-title":"TSE"},{"key":"10_CR24","unstructured":"IDAPro disassembler, http:\/\/www.datarescue.com\/idabase\/"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"Compiler Construction","author":"J. Knoop","year":"1992","unstructured":"Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Pfahler, P., Kastens, U. (eds.) CC 1992. LNCS, vol.\u00a0641, Springer, Heidelberg (1992)"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/978-3-540-31987-0_2","volume-title":"Programming Languages and Systems","author":"L. Mauborgne","year":"2005","unstructured":"Mauborgne, L., Rival, X.: Trace Partitioning in Abstract Interpretation Based Static Analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 5\u201320. Springer, Heidelberg (2005)"},{"key":"10_CR27","unstructured":"Oney, W.: Programming the Microsoft Windows Driver Model. In: Microsoft (2003)"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Ramalingam, G., Field, J., Tip, F.: Aggregate structure identification and its application to program analysis. In: POPL (1999)","DOI":"10.1145\/292540.292553"},{"key":"10_CR29","volume-title":"Program Flow Analysis: Theory and Applications","author":"M. Sharir","year":"1981","unstructured":"Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, Prentice-Hall, Englewood Cliffs (1981)"},{"key":"10_CR30","unstructured":"Swift, M.M., Annamalai, M., Bershad, B.N., Levy, H.M.: Recovering device drivers. In: OSDI (2004)"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Swift, M.M., Bershad, B.N., Levy, H.M.: Improving the reliability of commodity operating systems. ACM Trans. Comput. Syst.\u00a023(1) (2005)","DOI":"10.1145\/1047915.1047919"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78800-3_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:22:41Z","timestamp":1619508161000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78800-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540787990","9783540788003"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78800-3_10","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-540-78800-3","asserted-by":"object"}]},"subject":[]}}