{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,5]],"date-time":"2026-06-05T04:43:29Z","timestamp":1780634609883,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540691471","type":"print"},{"value":"9783540691495","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_22","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"202-213","source":"Crossref","is-referenced-by-count":37,"title":["WYSINWYX: What You See Is Not What You eXecute"],"prefix":"10.1007","author":[{"given":"G.","family":"Balakrishnan","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"T.","family":"Reps","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"D.","family":"Melski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"T.","family":"Teitelbaum","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"PREfast with driver-specific rules, Windows Hardware and Driver Central (WHDC) (October, 2004), http:\/\/www.microsoft.com\/whdc\/devtools\/tools\/PREfast-drv.mspx"},{"key":"22_CR2","unstructured":"Amme, W., Braun, P., Zehendner, E., Thomasset, F.: Data dependence analysis of assembly code. Int. J. Parallel Proc (2000)"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In: Comp. Construct. pp. 5\u201323 (2004)","DOI":"10.1007\/978-3-540-24723-4_2"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 260\u2013264. Springer, Heidelberg (2001)"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Boehm, H.-J.: Threads cannot be implemented as a library. In: PLDI, pp. 261\u2013268 (2005)","DOI":"10.1145\/1065010.1065042"},{"key":"22_CR6","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":"22_CR7","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. In: POPL, pp. 62\u201373 (2003)","DOI":"10.1145\/604131.604137"},{"key":"22_CR8","first-page":"775","volume":"30","author":"W. Bush","year":"2000","unstructured":"Bush, W., Pincus, J., Sielaff, D.: A static analyzer for finding dynamic programming errors. Software\u2013Practice&Experience\u00a030, 775\u2013802 (2000)","journal-title":"Software\u2013Practice&Experience"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Chen, H., Wagner, D.: MOPS: An infrastructure for examining security properties of software. In: Conf. on Comp. and Commun. Sec, November 2002, pp. 235\u2013244 (2002)","DOI":"10.1145\/586110.586142"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Cifuentes, C., Fraboulet, A.: Intraprocedural static slicing of binary executables. Int. Conf. on Softw. Maint. 188\u2013195 (1997)","DOI":"10.1109\/ICSM.1997.624245"},{"key":"22_CR11","unstructured":"CodeSurfer, GrammaTech, Inc. http:\/\/www.grammatech.com\/products\/codesurfer\/"},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S.: Bandera: Extracting finite-state models from Java source code. In: ICSE (2000)","DOI":"10.1145\/337180.337234"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: POPL (1977)","DOI":"10.1145\/512950.512973"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Coutant, D.S., Meloy, S., Ruscetta, M.: DOC: A practical approach to source-level debugging of globally optimized code. In: PLDI (1988)","DOI":"10.1145\/53990.54003"},{"key":"22_CR15","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\/512537.512538"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Debray, S.K., Muth, R., Weippert, M.: Alias analysis of executable code. In: POPL (1998)","DOI":"10.1145\/268946.268948"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Dwyer, M., Avrunin, G., Corbett, J.: Patterns in property specifications for finite-state verification. In: ICSE (1999)","DOI":"10.1145\/302405.302672"},{"key":"22_CR18","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: Op. Syst. Design and Impl. pp. 1\u201316 (2000)","DOI":"10.21236\/ADA419626"},{"key":"22_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":"22_CR20","unstructured":"Gerth, R.: Formal verification of self modifying code. In: Proc. Int. Conf. for Young Computer Scientists, pp. 305\u2013313 (1991)"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Gopan, D., Reps, T., Sagiv, M.: A framework for numeric analysis of array operations. In: POPL, pp. 338\u2013350 (2005)","DOI":"10.1145\/1040305.1040333"},{"key":"22_CR22","unstructured":"Guo, B., Bridges, M.J., Triantafyllis, S., Ottoni, G., Raman, E., August, D.I.: Practical and accurate low-level pointer analysis. In: 3nd Int. Symp. on Code Gen. and Opt (2005)"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Softw. Tools for Tech. Transfer\u00a02(4) (2000)","DOI":"10.1007\/s100090050043"},{"issue":"3","key":"22_CR24","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/357172.357173","volume":"4","author":"J.L. Hennessy","year":"1982","unstructured":"Hennessy, J.L.: Symbolic debugging of optimized code. Trans. on Prog. Lang. and Syst.\u00a04(3), 323\u2013344 (1982)","journal-title":"Trans. on Prog. Lang. and Syst."},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"issue":"1","key":"22_CR26","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/77606.77608","volume":"12","author":"S. Horwitz","year":"1990","unstructured":"Horwitz, S., Reps, T., Binkley, D.: Interprocedural slicing using dependence graphs. Trans. on Prog. Lang. and Syst.\u00a012(1), 26\u201360 (1990)","journal-title":"Trans. on Prog. Lang. and Syst."},{"key":"22_CR27","unstructured":"Howard, M.: Some bad news and some good news. In: MSDN (October, 2002), http:\/\/msdn.microsoft.com\/library\/default.asp?url=\/library\/en-us\/dncode\/html\/secure10102002.asp"},{"key":"22_CR28","unstructured":"IDAPro disassembler, http:\/\/www.datarescue.com\/idabase\/"},{"key":"22_CR29","unstructured":"Kidd, N., Reps, T., Melski, D., Lal, A.: WPDS++: A C++ library for weighted pushdown systems (2004), http:\/\/www.cs.wisc.edu\/wpis\/wpds++\/"},{"key":"22_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/11817963_32","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2006","unstructured":"Lal, A., Reps, T.: Improving pushdown system model checking. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 343\u2013357. Springer, Heidelberg (2006)"},{"key":"22_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/11513988_44","volume-title":"Computer Aided Verification","author":"A. Lal","year":"2005","unstructured":"Lal, A., Reps, T., Balakrishnan, G.: Extended weighted pushdown systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 434\u2013448. Springer, Heidelberg (2005)"},{"key":"22_CR32","doi-asserted-by":"crossref","unstructured":"Necula, G.: Translation validation for an optimizing compiler. In: PLDI (2000)","DOI":"10.1145\/349299.349314"},{"key":"22_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) ETAPS 1998 and TACAS 1998. LNCS, vol.\u00a01384, Springer, Heidelberg (1998)"},{"key":"22_CR34","doi-asserted-by":"crossref","unstructured":"Reps, T., Balakrishnan, G., Lim, J.: Intermediate-representation recovery from low-level code. In: Part. Eval. and Semantics-Based Prog. Manip (2006)","DOI":"10.1145\/1111542.1111560"},{"key":"22_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_11","volume-title":"Static Analysis","author":"T. Reps","year":"2003","unstructured":"Reps, T., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, Springer, Heidelberg (2003)"},{"issue":"1\u20132","key":"22_CR36","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1016\/j.scico.2005.02.009","volume":"58","author":"T. Reps","year":"2005","unstructured":"Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. of Comp. Prog.\u00a058(1\u20132), 206\u2013263 (2005)","journal-title":"Sci. of Comp. Prog."},{"key":"22_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-36384-X_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"X. Rival","year":"2002","unstructured":"Rival, X.: Abstract interpretation based certification of assembly code. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 41\u201355. Springer, Heidelberg (2002)"},{"key":"22_CR38","unstructured":"Schwoon, S.: Moped system, http:\/\/www.fmi.uni-stuttgart.de\/szs\/tools\/moped\/"},{"key":"22_CR39","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technical Univ. of Munich, Munich, Germany (July, 2002)"},{"key":"22_CR40","first-page":"189","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: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, ch.\u00a07, pp. 189\u2013234. Prentice-Hall, Englewood Cliffs (1981)"},{"key":"22_CR41","unstructured":"Wagner, D., Foster, J., Brewer, E., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. In: Network and Dist. Syst. Security (February, 2000)"},{"key":"22_CR42","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-1-4471-3501-2_15","volume-title":"Code Generation \u2013 Concepts, Tools, Techniques","author":"D.W. Wall","year":"1992","unstructured":"Wall, D.W.: Systems for late code modification. In: Giegerich, R., Graham, S.L. (eds.) Code Generation \u2013 Concepts, Tools, Techniques, pp. 275\u2013293. Springer, Heidelberg (1992)"},{"key":"22_CR43","doi-asserted-by":"crossref","unstructured":"Wilson, R.P., Lam, M.S.: Efficient context-sensitive pointer analysis for C programs. In: PLDI, pp. 1\u201312 (1995)","DOI":"10.1145\/207110.207111"},{"key":"22_CR44","unstructured":"Zellweger, P.T.: Interactive Source-Level Debugging of Optimized Programs. PhD thesis, Univ. of California, Berkeley (1984)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,19]],"date-time":"2023-05-19T10:44:12Z","timestamp":1684493052000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}