{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T20:32:23Z","timestamp":1725481943946},"publisher-location":"Boston, MA","reference-count":46,"publisher":"Springer US","isbn-type":[{"type":"print","value":"9780387327204"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-0-387-44599-1_3","type":"book-chapter","created":{"date-parts":[[2007,3,4]],"date-time":"2007-03-04T15:35:08Z","timestamp":1173022508000},"page":"43-61","source":"Crossref","is-referenced-by-count":2,"title":["A Next-Generation Platform for Analyzing Executables"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Reps","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gogul","family":"Balakrishnan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Junghee","family":"Lim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim","family":"Teitelbaum","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"..*. PREfast with driver-specific rules, Oct. 2004. WHDC, Microsoft Corp., http:\/\/www.microsoft.com\/whdc\/devtools\/tools\/PREfast-dm.mspx."},{"key":"3_CR2","unstructured":"W. Amme, P. Braun, E. Zehendner, and E Thomasset. Data dependence analysis of assembly code. Int. J. Parallel Proc., 2000."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"G. Balakrishnan and T. Reps. Analyzing memory accesses in x86 executables. In Comp. Construct., pages 5\u201323,2004.","DOI":"10.1007\/978-3-540-24723-4_2"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"G. Balakrishnan and T. Reps. Recency-abstraction for heap-allocated storage. In Static Analysis Symp., 2006.","DOI":"10.1007\/11823230_15"},{"key":"3_CR5","unstructured":"G. Balakrishnan, T. Reps, D. Melski, and T. Teitelbaum. WYSINWYX: What You See Is Not What You execute. In IFIP Working Conf. on Verified Software: Theories, Tools, Experiments, 2005."},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"T. Ball and S. Rajamani. The SLAM toolkit. In Computer Aided Verit., volume 2102 of Lec. Notes in Comp. Sci., pages 260\u2013264,2001.","DOI":"10.1007\/3-540-44585-4_25"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J. Esparza, and 0. Maler. Reachability analysis of pushdown automata: Application to model checking. In Proc. CONCUR, volume 1243 of Lec. Notes in Comp. Sci., pages 135\u2013150. Springer-Verlag, 1997.","DOI":"10.1007\/3-540-63141-0_10"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis of concurrent programs with procedures. In Princ. of Prog. Lung., pages 62\u201373,2003.","DOI":"10.1145\/640128.604137"},{"key":"3_CR9","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":"W. Bush, J. Pincus, and D. Sielaff. A static analyzer for finding dynamic programming errors. Software-Practice & Experience, 30:775\u2013802,2000.","journal-title":"Software-Practice & Experience"},{"key":"3_CR10","unstructured":"H. Chen, D. Dean, and D. Wagner. Model checking one million lines of C code. In Network and Dist. Syst. Security, 2004."},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"H. Chen and D. Wagner. MOPS: An infrastructure for examining security properties of software. In Conf on Comp. and Commun. Sec., pages 235\u2013244, Nov. 2002.","DOI":"10.1145\/586110.586142"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"C. Cifuentes and A. Fraboulet. Intraprocedural static slicing of binary executables. In Int. Conf on Softw. Maint., pages 188\u2013195,1997.","DOI":"10.1109\/ICSM.1997.624245"},{"key":"3_CR13","unstructured":"E. Clarke, Jr., 0. Grumberg, and D. Peled. Model Checking. The M.I.T. Press, 1999."},{"key":"3_CR14","unstructured":"Codesurfer, GrammaTech, Inc., http:llwww.grammatech.comlproductslcodesurferl."},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"J. Corbett, M. Dwyer, J. Hatcliff, S. Laubach, C. Pasareanu, Robby, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Int. Con$ on Softw. Eng., pages 439\u2013448,2000.","DOI":"10.1145\/337180.337234"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In Princ. of Prog. Lung., pages 238\u2013252, 1977.","DOI":"10.1145\/512950.512973"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"D. Coutant, S. Meloy, and M. Ruscetta. DOC: A practical approach to source-level debugging of globally optimized code. In Prog. Lung. Design and Impl., 1988.","DOI":"10.1145\/53990.54003"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification in polynomial time. In Prog. Lang. Design and Impl., pages 57\u201368, New York, NY, 2002. ACM Press.","DOI":"10.1145\/543552.512538"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"S. Debray, R. Muth, and M. Weippert. Alias analysis of executable code. In Princ. of Prog. Lung., pages 12\u201324,1998.","DOI":"10.1145\/268946.268948"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"M. Dwyer, G. Avrunin, and J. Corbett. Patterns in property specifications for finite-state verification. In Int. Conf on Softw. Eng., 1999.","DOI":"10.1145\/302405.302672"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using systemspecific, programmer-written compiler extensions. In Op. Syst. Design and Impl., pages 1\u201316,2000.","DOI":"10.21236\/ADA419626"},{"issue":"9","key":"3_CR22","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/24039.24041","volume":"3","author":"J. Ferrante","year":"1987","unstructured":"J. Ferrante, K. Ottenstein, and J. Warren. The program dependence graph and its use in optimization. Trans. on Prog. Lung. and Syst., 3(9):319\u2013349, 1987.","journal-title":"Trans. on Prog. Lung. and Syst."},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model checking pushdown systems. Elec. Notes in Theor. Comp. Sci., 9, 1997.","DOI":"10.1016\/S1571-0661(05)80426-8"},{"key":"3_CR24","unstructured":"Fast Library Identification and Recognition Technology, DataRescue sa\/nv, Li\u00e8ge, Belgium, http:l\/www.datarescue.comlidabase\/flirt.htm."},{"key":"3_CR25","unstructured":"B. Guo, M. Bridges, S. Triantafyllis, G. Ottoni, E. Raman, and D. August. Practical and accurate low-level pointer analysis. In 3nd Int. Symp. on Code Gen. and Opt., pages 291\u2013302,2005."},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"K. Havelund and T. Pressburger. Model checking Java programs using Java PathFinder. Softw. Tools for Tech. Transfer, 2(4), 2000.","DOI":"10.1007\/s100090050043"},{"issue":"3","key":"3_CR27","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/357172.357173","volume":"4","author":"J. Hennessy","year":"1982","unstructured":"J. Hennessy. Symbolic debugging of optimized code. Trans. on Prog. Lung. and Syst., 4(3):323\u2013344, 1982.","journal-title":"Trans. on Prog. Lung. and Syst."},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"T. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In Princ. of Prog. Lung., pages 58\u201370,2002.","DOI":"10.1145\/565816.503279"},{"issue":"1","key":"3_CR29","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/77606.77608","volume":"12","author":"S. Honvitz","year":"1990","unstructured":"S. Honvitz, T. Reps, and D. Binkley. Interprocedural slicing using dependence graphs. Trans. on Prog. Lang. and Syst., 12(1):26\u201360, Jan. 1990.","journal-title":"Trans. on Prog. Lang. and Syst."},{"key":"3_CR30","unstructured":"M. Howard. Some bad news and some good news. Oct. 2002. MSDN, Microsoft Corp., http:\/\/msdn.microsoft.com\/library\/default.asp?url=\/library\/enus\/dncode\/htm\/secure10102002.asp."},{"key":"3_CR31","unstructured":"IDAPro disassembler, http:\/\/www.datarescue.com\/idabase\/."},{"key":"3_CR32","unstructured":"N. Kidd, T. Reps, D. Melski, and A. Lal. WPDS++: A C++ library for weighted pushdown systems, 2004. http:\/\/www.cs.wisc.edu\/wpis\/wpds++\/."},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"A. Lal, T. Reps, and G. Balakrishnan. Extended weighted pushdown systems. In Computer Aided Verif, 2005.","DOI":"10.1007\/11513988_44"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"M. Miiller-Olm and H. Seidl. Analysis of modular arithmetic. In European Symp. on Programming, 2005.","DOI":"10.1007\/978-3-540-31987-0_5"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"G. Ramalingam, J. Field, and F. Tip. Aggregate structure identification and its application to program analysis. In Princ. of Prog. Lung., pages 119\u2013132,1999.","DOI":"10.1145\/292540.292553"},{"key":"3_CR36","doi-asserted-by":"crossref","unstructured":"T. Reps, G. Balakrishnan, and J. Lim. Intermediate-representation recovery from lowlevel code. In Part. Eval. and Semantics-Based Prog. Manip., 2006.","DOI":"10.1145\/1111542.1111560"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"T. Reps, G. Balakrishnan, J. Lim, and T. Teitelbaum. A next-generation platform for analyzing executables. In Asian Symp. on Prog. Lung. and Systems, 2005.","DOI":"10.1007\/11575467_15"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"T. Reps and G. Rosay. Precise interprocedural chopping. In Found. of Softw. Eng., 1995.","DOI":"10.1145\/222124.222138"},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"T. Reps, S. Schwoon, and S. Jha. Weighted pushdown systems and their application to interprocedural dataflow analysis. In Static Analysis Symp., 2003.","DOI":"10.1007\/3-540-44898-5_11"},{"issue":"1-2","key":"3_CR40","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1016\/j.scico.2005.02.009","volume":"58","author":"T. Reps","year":"2005","unstructured":"T. Reps, S. Schwoon, S. Jha, and D. Melski. Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. of Comp. Prog., 58(1-2):206\u2013263, Oct. 2005.","journal-title":"Sci. of Comp. Prog."},{"key":"3_CR41","unstructured":"S. Schwoon. Moped system. http:\/\/www.fmi.uni-stuttgart.de\/szs\/tools\/mopedl."},{"key":"3_CR42","series-title":"PhD thesis","volume-title":"Model-Checking Pushdown Systems","author":"S. Schwoon","year":"2002","unstructured":"S. Schwoon. Model-Checking Pushdown Systems. PhD thesis, Technical Univ. of Munich, Munich, Germany, July 2002."},{"key":"3_CR43","unstructured":"D. Wagner, J. Foster, E. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In Network and Dist. Syst. Security, Feb. 2000."},{"key":"3_CR44","doi-asserted-by":"crossref","unstructured":"D. Wall. Systems for late code modification. In R. Giegerich and S. Graham, editors, Code Generation-Concepts, Tools, Techniques, pages 275\u2013293. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4471-3501-2_15"},{"key":"3_CR45","doi-asserted-by":"crossref","unstructured":"R. Wilson and M. Lam. Efficient context-sensitive pointer analysis for C programs. In Prog. Lung. Design and Impl., pages 1\u201312,1995.","DOI":"10.1145\/207110.207111"},{"key":"3_CR46","series-title":"PhD thesis","volume-title":"Interactive Source-Level Debugging of Optimized Programs","author":"P. Zellweger","year":"1984","unstructured":"P. Zellweger. Interactive Source-Level Debugging of Optimized Programs. PhD thesis, Univ. of California, Berkeley, 1984."}],"container-title":["Advances in Information Security","Malware Detection"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-0-387-44599-1_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T02:00:35Z","timestamp":1619575235000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-0-387-44599-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9780387327204"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/978-0-387-44599-1_3","relation":{},"subject":[]}}