{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,18]],"date-time":"2026-09-18T16:47:10Z","timestamp":1789750030812,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540297352","type":"print"},{"value":"9783540322474","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11575467_15","type":"book-chapter","created":{"date-parts":[[2005,11,11]],"date-time":"2005-11-11T08:58:51Z","timestamp":1131699531000},"page":"212-229","source":"Crossref","is-referenced-by-count":19,"title":["A Next-Generation Platform for Analyzing Executables"],"prefix":"10.1007","author":[{"given":"T.","family":"Reps","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"G.","family":"Balakrishnan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J.","family":"Lim","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"T.","family":"Teitelbaum","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"15_CR1","unstructured":"PREfast with driver-specific rules (October 2004) WHDC, Microsoft Corp., http:\/\/www.microsoft.com\/whdc\/devtools\/tools\/PREfast-drv.mspx"},{"key":"15_CR2","unstructured":"Amme, W., Braun, P., Zehendner, E., Thomasset, F.: Data dependence analysis of assembly code. Int. J. Parallel Proc. (2000)"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. Comp. Construct., 5\u201323 (2004)","DOI":"10.1007\/978-3-540-24723-4_2"},{"key":"15_CR4","unstructured":"Balakrishnan, G., Reps, T., Melski, D., Teitelbaum, T.: WYSINWYX: What You See Is Not What You eXecute. In: IFIP Working Conf. on Verified Software: Theories, Tools, Experiments (2005)"},{"key":"15_CR5","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":"15_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"Proc. CONCUR","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model checking. In: Proc. CONCUR. LNCS, vol.\u00a01243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"15_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: Princ. of Prog. Lang., pp. 62\u201373 (2003)","DOI":"10.1145\/604131.604137"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"775","DOI":"10.1002\/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H","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":"15_CR9","unstructured":"Chen, H., Dean, D., Wagner, D.: Model checking one million lines of C code. Network and Dist. Syst. Security (2004)"},{"key":"15_CR10","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":"15_CR11","doi-asserted-by":"crossref","unstructured":"Cifuentes, C., Fraboulet, A.: Intraprocedural static slicing of binary executables. In: Int. Conf. on Softw. Maint., pp. 188\u2013195 (1997)","DOI":"10.1109\/ICSM.1997.624245"},{"key":"15_CR12","volume-title":"Model Checking","author":"E.M. Clarke Jr.","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"15_CR13","unstructured":"CodeSurfer, GrammaTech, Inc., http:\/\/www.grammatech.com\/products\/codesurfer\/"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Robby, C.S.P. , Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: Int. Conf. on Softw. Eng., pp. 439\u2013448 (2000)","DOI":"10.1145\/337180.337234"},{"key":"15_CR15","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: Princ. of Prog. Lang., pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"15_CR16","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: Prog. Lang. Design and Impl. (1988)","DOI":"10.1145\/53990.54003"},{"key":"15_CR17","first-page":"57","volume-title":"Prog. Lang. Design and Impl.","author":"M. Das","year":"2002","unstructured":"Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: Prog. Lang. Design and Impl., pp. 57\u201368. ACM Press, New York (2002)"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"Debray, S.K., Muth, R., Weippert, M.: Alias analysis of executable code. In: Princ. of Prog. Lang., pp. 12\u201324 (1998)","DOI":"10.1145\/268946.268948"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Dwyer, M., Avrunin, G., Corbett, J.: Patterns in property specifications for finite-state verification. In: Int. Conf. on Softw. Eng. (1999)","DOI":"10.1145\/302405.302672"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Engler, D.R., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. Op. Syst. Design and Impl., 1\u201316 (2000)","DOI":"10.21236\/ADA419626"},{"issue":"9","key":"15_CR21","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/24039.24041","volume":"3","author":"J. Ferrante","year":"1987","unstructured":"Ferrante, J., Ottenstein, K., Warren, J.: The program dependence graph and its use in optimization. Trans. on Prog. Lang. and Syst.\u00a03(9), 319\u2013349 (1987)","journal-title":"Trans. on Prog. Lang. and Syst."},{"key":"15_CR22","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":"15_CR23","unstructured":"Fast Library Identification and Recognition Technology, DataRescue sa\/nv, Li\u00e8ge, Belgium, http:\/\/www.datarescue.com\/idabase\/flirt.htm"},{"key":"15_CR24","unstructured":"Guo, B., Bridges, M.J., Triantafyllis, S., Ottoni, G., Raman, E., August, D.I.: Practical and accurate low-level pointer analysis. In: 3rd Int. Symp. on Code Gen. and Opt., pp. 291\u2013302 (2005)"},{"key":"15_CR25","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":"15_CR26","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":"15_CR27","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Princ. of Prog. Lang., pp. 58\u201370 (2002)","DOI":"10.1145\/503272.503279"},{"issue":"1","key":"15_CR28","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":"15_CR29","unstructured":"Howard, M.: Some bad news and some good news (October 2002) MSDN, Microsoft Corp., http:\/\/msdn.microsoft.com\/library\/default.asp?url=\/library\/en-us\/dncode\/html\/secure10102002.asp"},{"key":"15_CR30","unstructured":"IDAPro disassembler, http:\/\/www.datarescue.com\/idabase\/"},{"key":"15_CR31","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":"15_CR32","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":"15_CR33","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Analysis of modular arithmetic. In: European Symp. on Programming (2005)","DOI":"10.1007\/978-3-540-31987-0_5"},{"key":"15_CR34","doi-asserted-by":"crossref","unstructured":"Ramalingam, G., Field, J., Tip, F.: Aggregate structure identification and its application to program analysis. In: Princ. of Prog. Lang., pp. 119\u2013132 (1999)","DOI":"10.1145\/292540.292553"},{"key":"15_CR35","doi-asserted-by":"crossref","unstructured":"Reps, T., Rosay, G.: Precise interprocedural chopping. In: Found. of Softw. Eng. (1995)","DOI":"10.1145\/222124.222138"},{"key":"15_CR36","doi-asserted-by":"crossref","unstructured":"Reps, T., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Static Analysis Symp. (2003)","DOI":"10.1007\/3-540-44898-5_11"},{"key":"15_CR37","doi-asserted-by":"crossref","unstructured":"Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Sci. of Comp. Prog. (to appear)","DOI":"10.21236\/ADA449102"},{"key":"15_CR38","unstructured":"Schwoon, S.: Moped system, http:\/\/www.fmi.uni-stuttgart.de\/szs\/tools\/moped\/"},{"key":"15_CR39","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technical Univ. of Munich, Munich, Germany (July 2002)"},{"key":"15_CR40","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":"15_CR41","doi-asserted-by":"crossref","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":"15_CR42","doi-asserted-by":"crossref","unstructured":"Wilson, R.P., Lam, M.S.: Efficient context-sensitive pointer analysis for C programs. In: Prog. Lang. Design and Impl., pp. 1\u201312 (1995)","DOI":"10.1145\/207110.207111"},{"key":"15_CR43","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","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11575467_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T06:41:49Z","timestamp":1683268909000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11575467_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540297352","9783540322474"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/11575467_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}