{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T22:01:55Z","timestamp":1791237715008,"version":"4.1.0"},"reference-count":108,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2013,4,1]],"date-time":"2013-04-01T00:00:00Z","timestamp":1364774400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","award":["FA8750-05-C-0179, FA8750-06-C-0249, FA9550-09-1-0279, FA8650-10-C-7088"],"award-info":[{"award-number":["FA8750-05-C-0179, FA8750-06-C-0249, FA9550-09-1-0279, FA8650-10-C-7088"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-01-1-0708, N00014-01-1-0796, N00014-09-1-0510, N00014-09-1-0776, N00014-10-M-0251, N00014-11-C-0447"],"award-info":[{"award-number":["N00014-01-1-0708, N00014-01-1-0796, N00014-09-1-0510, N00014-09-1-0776, N00014-10-M-0251, N00014-11-C-0447"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006754","name":"U.S. Army Research Laboratory","doi-asserted-by":"publisher","award":["W911NF-09-1-0413"],"award-info":[{"award-number":["W911NF-09-1-0413"]}],"id":[{"id":"10.13039\/100006754","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR0011-12-2-0012"],"award-info":[{"award-number":["HR0011-12-2-0012"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"name":"GrammaTech, Inc."},{"name":"Symantec Research Labs Graduate Fellowship"},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-0524051, CCF-0540955, CCF-0810053, CCF-0904371"],"award-info":[{"award-number":["CCF-0524051, CCF-0540955, CCF-0810053, CCF-0904371"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2013,4]]},"abstract":"<jats:p>\n            This article describes the design and implementation of a system, called T\n            <jats:sc>SL<\/jats:sc>\n            (for Transformer Specification Language), that provides a systematic solution to the problem of creating retargetable tools for analyzing machine code. T\n            <jats:sc>SL<\/jats:sc>\n            is a tool generator---that is, a metatool---that automatically creates different abstract interpreters for machine-code instruction sets.\n          <\/jats:p>\n          <jats:p>\n            The most challenging technical issue that we faced in designing T\n            <jats:sc>SL<\/jats:sc>\n            was how to automate the generation of the set of\n            <jats:italic>abstract transformers<\/jats:italic>\n            for a given abstract interpretation of a given instruction set. From a description of the\n            <jats:italic>concrete operational semantics<\/jats:italic>\n            of an instruction set, together with the datatypes and operations that define an abstract domain, T\n            <jats:sc>SL<\/jats:sc>\n            automatically creates the set of abstract transformers for the instructions of the instruction set. T\n            <jats:sc>SL<\/jats:sc>\n            advances the state-of-the-art in program analysis because it provides two dimensions of parameterizability: (i) a given analysis component can be retargeted to different instruction sets; (ii) multiple analysis components can be created automatically from a single specification of the concrete operational semantics of the language to be analyzed.\n          <\/jats:p>\n          <jats:p>\n            T\n            <jats:sc>SL<\/jats:sc>\n            is an\n            <jats:italic>abstract-transformer-generator generator<\/jats:italic>\n            . The article describes the principles behind T\n            <jats:sc>SL<\/jats:sc>\n            , and discusses how one uses T\n            <jats:sc>SL<\/jats:sc>\n            to develop different abstract interpreters.\n          <\/jats:p>","DOI":"10.1145\/2450136.2450139","type":"journal-article","created":{"date-parts":[[2013,5,1]],"date-time":"2013-05-01T19:47:09Z","timestamp":1367437629000},"page":"1-59","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":38,"title":["TSL"],"prefix":"10.1145","volume":"35","author":[{"given":"Junghee","family":"Lim","sequence":"first","affiliation":[{"name":"University of Wisconsin"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin and GrammaTech, Inc."}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2013,4]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the Statistical Analysis Symposium (SAS\u201995)","volume":"983","author":"Alt M.","unstructured":"Alt , M. and Martin , F . 1995. Generation of efficient interprocedural analyzers with PAG . In Proceedings of the Statistical Analysis Symposium (SAS\u201995) . Lecture Notes in Computer Science , vol. 983 . Springer, 33--50. Alt, M. and Martin, F. 1995. Generation of efficient interprocedural analyzers with PAG. In Proceedings of the Statistical Analysis Symposium (SAS\u201995). Lecture Notes in Computer Science, vol. 983. Springer, 33--50."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/11779148_1"},{"key":"e_1_2_1_3_1","unstructured":"APRON. 2007. APRON numerical abstract domain library. apron.cri.ensmp.fr.  APRON. 2007. APRON numerical abstract domain library. apron.cri.ensmp.fr."},{"key":"e_1_2_1_4_1","unstructured":"ARMv7-A 2013. ARMv7-A in HOL. github.com\/mn200\/HOL\/tree\/master\/examples\/ARM\/v7.  ARMv7-A 2013. ARMv7-A in HOL. github.com\/mn200\/HOL\/tree\/master\/examples\/ARM\/v7."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/363911.363914"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","unstructured":"Balakrishnan G. 2007. WYSINWYX: What you see is not what you execute. Ph.D. thesis Computer Science Department University of Wisconsin Madison WI. Tech. rep. 1603.   Balakrishnan G. 2007. WYSINWYX: What you see is not what you execute. Ph.D. thesis Computer Science Department University of Wisconsin Madison WI. Tech. rep. 1603.","DOI":"10.1007\/978-3-540-69149-5_22"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the International Conference on Compiler Construction (CC\u201904)","author":"Balakrishnan G.","unstructured":"Balakrishnan , G. and Reps , T . 2004. Analyzing memory accesses in x86 executables . In Proceedings of the International Conference on Compiler Construction (CC\u201904) . 5--23. Balakrishnan, G. and Reps, T. 2004. Analyzing memory accesses in x86 executables. In Proceedings of the International Conference on Compiler Construction (CC\u201904). 5--23."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201907)","author":"Balakrishnan G.","unstructured":"Balakrishnan , G. and Reps , T . 2007. DIVINE: Discovering variables in executables . In Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201907) . 1--28. Balakrishnan, G. and Reps, T. 2007. DIVINE: Discovering variables in executables. In Proceedings of the 8th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201907). 1--28."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1749608.1749612"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31985-6_19"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390634"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604137"},{"key":"e_1_2_1_13_1","first-page":"3","article-title":"Transfer function synthesis without quantiffer elimination","volume":"8","author":"Brauer J.","year":"2012","unstructured":"Brauer , J. and King , A. 2012 . Transfer function synthesis without quantiffer elimination . Logic. Methods Comput. Sci. 8 , 3 . Brauer, J. and King, A. 2012. Transfer function synthesis without quantiffer elimination. Logic. Methods Comput. Sci. 8, 3.","journal-title":"Logic. Methods Comput. Sci."},{"key":"e_1_2_1_14_1","unstructured":"Brauer J. King A. and Kowalewski S. 2012. Abstract interpretation of microcontroller code: Intervals meet congruences. Sci. Comput. Program. 77. To appear.  Brauer J. King A. and Kowalewski S. 2012. Abstract interpretation of microcontroller code: Intervals meet congruences. Sci. Comput. Program. 77 . To appear."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the Conference on Computer Aided Verification (CAV\u201911)","author":"Brumley D.","unstructured":"Brumley , D. , Jager , I. , Avgerinos , T. , and Schwartz , E . 2011. BAP: A binary analysis platform . In Proceedings of the Conference on Computer Aided Verification (CAV\u201911) . Brumley, D., Jager, I., Avgerinos, T., and Schwartz, E. 2011. BAP: A binary analysis platform. In Proceedings of the Conference on Computer Aided Verification (CAV\u201911)."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/12.1.41"},{"key":"e_1_2_1_17_1","unstructured":"Cok D. 2010. Safety in numbers. www.dtic.mil\/dtic\/tr\/fulltext\/u2\/a532995.pdf.  Cok D. 2010. Safety in numbers. www.dtic.mil\/dtic\/tr\/fulltext\/u2\/a532995.pdf."},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the Design Automation Conference (DAC\u201993)","author":"Cook T. A.","unstructured":"Cook , T. A. , Franzon , P. D. , Harcourt , E. A. , and Miller , T. K . 1993. System-level specification of instruction sets . In Proceedings of the Design Automation Conference (DAC\u201993) . Cook, T. A., Franzon, P. D., Harcourt, E. A., and Miller, T. K. 1993. System-level specification of instruction sets. In Proceedings of the Design Automation Conference (DAC\u201993)."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.53996"},{"key":"e_1_2_1_20_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the International Symposium on Verification, Theory and Practice, Honoring Zohar Manna\u2019s 64th Birthday","author":"Cousot P.","unstructured":"Cousot , P. 2003. Verification by abstract interpretation . In Proceedings of the International Symposium on Verification, Theory and Practice, Honoring Zohar Manna\u2019s 64th Birthday . Lecture Notes in Computer Science , vol. 2772 , Springer , 243--268. Cousot, P. 2003. Verification by abstract interpretation. In Proceedings of the International Symposium on Verification, Theory and Practice, Honoring Zohar Manna\u2019s 64th Birthday. Lecture Notes in Computer Science, vol. 2772, Springer, 243--268."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325699"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1780.1783"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 337--340","author":"de Moura L.","unstructured":"de Moura , L. and Bj\u00f8rner , N . 2008. Z3: An efficient SMT solver . In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 337--340 . de Moura, L. and Bj\u00f8rner, N. 2008. Z3: An efficient SMT solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 337--340."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_47"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the CanSecWest Applied Security Conference.","author":"Dullien T.","unstructured":"Dullien , T. and Porst , S . 2009. REIL: A platform-independent intermediate representation of disassembled code for static code analysis . In Proceedings of the CanSecWest Applied Security Conference. Dullien, T. and Porst, S. 2009. REIL: A platform-independent intermediate representation of disassembled code for static code analysis. In Proceedings of the CanSecWest Applied Security Conference."},{"key":"e_1_2_1_29_1","volume-title":"Yices: An SMT solver. yices.csl.sri.com.","author":"Dutertre B.","year":"2006","unstructured":"Dutertre , B. and de Moura , L. 2006 . Yices: An SMT solver. yices.csl.sri.com. Dutertre, B. and de Moura, L. 2006. Yices: An SMT solver. yices.csl.sri.com."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041569"},{"key":"e_1_2_1_31_1","unstructured":"Elder M. Lim J. Sharma T. Andersen T. and Reps T. 2013. Abstract domains of affine relations. Tech. rep. TR-1777 Computer Science Department University of Wisconsin Madison WI.  Elder M. Lim J. Sharma T. Andersen T. and Reps T. 2013. Abstract domains of affine relations. Tech. rep. TR-1777 Computer Science Department University of Wisconsin Madison WI."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/24039.24041"},{"key":"e_1_2_1_33_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics","author":"Fox A.","unstructured":"Fox , A. 2003. Formal specification and verification of ARM6 . In Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics . Lecture Notes in Computer Science , vol. 2758 , Springer , 25--40. Fox, A. 2003. Formal specification and verification of ARM6. In Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 2758, Springer, 25--40."},{"key":"e_1_2_1_34_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the International Conference on Interactive Theorem Proving","author":"Fox A.","unstructured":"Fox , A. 2012. Directions in ISA specification . In Proceedings of the International Conference on Interactive Theorem Proving . Lecture Notes in Computer Science , vol. 7406 , Springer , 338--344. Fox, A. 2012. Directions in ISA specification. In Proceedings of the International Conference on Interactive Theorem Proving. Lecture Notes in Computer Science, vol. 7406, Springer, 338--344."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_18"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.733618"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181790"},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the International Conference on Simulation and Hardware Description Languages.","author":"Harcourt E.","unstructured":"Harcourt , E. , Mauney , J. , and Cook , T . 1994. Functional specification and simulation of instruction set architectures . In Proceedings of the International Conference on Simulation and Hardware Description Languages. Harcourt, E., Mauney, J., and Cook, T. 1994. Functional specification and simulation of instruction set architectures. In Proceedings of the International Conference on Simulation and Hardware Description Languages."},{"key":"e_1_2_1_40_1","unstructured":"IA32. 1999. Intel architecture software developer\u2019s manual. developer.intel.com\/design\/pentiumii\/manuals\/243191.htm.  IA32. 1999. Intel architecture software developer\u2019s manual. developer.intel.com\/design\/pentiumii\/manuals\/243191.htm."},{"key":"e_1_2_1_41_1","volume-title":"Intel 64 and IA-32 architectures software developer\u2019s manual","author":"Intel","unstructured":"Intel . 2013a. Intel 64 and IA-32 architectures software developer\u2019s manual , Vol. 2A: Instruction set reference, A-M. Intel. download.intel.com\/design\/processor\/manuals\/ 253666 .pdf. Intel. 2013a. Intel 64 and IA-32 architectures software developer\u2019s manual, Vol. 2A: Instruction set reference, A-M. Intel. download.intel.com\/design\/processor\/manuals\/253666.pdf."},{"key":"e_1_2_1_42_1","volume-title":"Intel 64 and IA-32 architectures software developer\u2019s manual","author":"Intel","unstructured":"Intel . 2013b. Intel 64 and IA-32 architectures software developer\u2019s manual , Vol. 2B: Instruction set reference, N-Z. Intel. download.intel.com\/design\/processor\/manuals\/ 253667 .pdf. Intel. 2013b. Intel 64 and IA-32 architectures software developer\u2019s manual, Vol. 2B: Instruction set reference, N-Z. Intel. download.intel.com\/design\/processor\/manuals\/253667.pdf."},{"key":"e_1_2_1_43_1","volume-title":"YACC: Yet another compiler-compiler. Tech. rep. 32, Bell Laboratories.","author":"Johnson S.","year":"1975","unstructured":"Johnson , S. 1975 . YACC: Yet another compiler-compiler. Tech. rep. 32, Bell Laboratories. Johnson, S. 1975. YACC: Yet another compiler-compiler. Tech. rep. 32, Bell Laboratories."},{"key":"e_1_2_1_44_1","unstructured":"Jones N. Gomard C. and Sestoft P. 1993. Partial Evaluation and Automatic Program Generation. Prentice-Hall International.   Jones N. Gomard C. and Sestoft P. 1993. Partial Evaluation and Automatic Program Generation . Prentice-Hall International."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512672"},{"key":"e_1_2_1_46_1","volume-title":"Maibaum Eds.","volume":"4","author":"Jones N.","unstructured":"Jones , N. and Nielson , F . 1995. Abstract interpretation: A semantics-based tool for program analysis. In Handbook of Logic in Computer Science, S. Abramsky, D. Gabbay, and T . Maibaum Eds. , Vol. 4 , Oxford University Press, 527--636. Jones, N. and Nielson, F. 1995. Abstract interpretation: A semantics-based tool for program analysis. In Handbook of Logic in Computer Science, S. Abramsky, D. Gabbay, and T. Maibaum Eds., Vol. 4, Oxford University Press, 527--636."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/954186.954188"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_16"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_16"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:LISP.0000029444.99264.c0"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_32"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_44"},{"key":"e_1_2_1_53_1","volume-title":"Cetus Users and Compiler Infrastructure Workshop.","author":"Lam P.","unstructured":"Lam , P. , Bodden , E. , Lhotak , O. , and Hendren , L . 2011. The SOOT framework for Java program analysis: A retrospective . In Cetus Users and Compiler Infrastructure Workshop. Lam, P., Bodden, E., Lhotak, O., and Hendren, L. 2011. The SOOT framework for Java program analysis: A retrospective. In Cetus Users and Compiler Infrastructure Workshop."},{"key":"e_1_2_1_54_1","volume-title":"International Symposium on Code Generation and Optimization.","author":"Lattner C.","unstructured":"Lattner , C. and Adve , V . 2004. LLVM: A compilation framework for lifelong program analysis and transformation . In International Symposium on Code Generation and Optimization. Lattner, C. and Adve, V. 2004. LLVM: A compilation framework for lifelong program analysis and transformation. In International Symposium on Code Generation and Optimization."},{"key":"e_1_2_1_55_1","volume-title":"Proceedings of the 7th International Symposium on Static Analysis (SAS\u201900)","author":"Lev-Ami T.","unstructured":"Lev-Ami , T. and Sagiv , M . 2000. TVLA: A system for implementing static analyses . In Proceedings of the 7th International Symposium on Static Analysis (SAS\u201900) . 280--301. Lev-Ami, T. and Sagiv, M. 2000. TVLA: A system for implementing static analyses. In Proceedings of the 7th International Symposium on Static Analysis (SAS\u201900). 280--301."},{"key":"e_1_2_1_56_1","volume-title":"Computer Science Department","author":"Lim J.","unstructured":"Lim , J. 2011. Transformer specification language: A system for generating analyzers and its applications. Tech. rep. 1689 , Computer Science Department , University of Wisconsin , Madison, WI . Lim, J. 2011. Transformer specification language: A system for generating analyzers and its applications. Tech. rep. 1689, Computer Science Department, University of Wisconsin, Madison, WI."},{"key":"e_1_2_1_57_1","volume-title":"Proceedings of the Joint European Conferences on Theory and Practice of Software, 17th International Conference on Compiler Construction. 36--52","author":"Lim J.","unstructured":"Lim , J. and Reps , T . 2008. A system for generating static analyzers for machine instructions . In Proceedings of the Joint European Conferences on Theory and Practice of Software, 17th International Conference on Compiler Construction. 36--52 . Lim, J. and Reps, T. 2008. A system for generating static analyzers for machine instructions. In Proceedings of the Joint European Conferences on Theory and Practice of Software, 17th International Conference on Compiler Construction. 36--52."},{"key":"e_1_2_1_58_1","volume-title":"BCE: Extracting botnet commands from bot executables. Tech. rep. TR-1668, Computer Science Department","author":"Lim J.","year":"2010","unstructured":"Lim , J. and Reps , T . 2010 . BCE: Extracting botnet commands from bot executables. Tech. rep. TR-1668, Computer Science Department , University of Wisconsin , Madison, WI . Lim, J. and Reps, T. 2010. BCE: Extracting botnet commands from bot executables. Tech. rep. TR-1668, Computer Science Department, University of Wisconsin, Madison, WI."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02652-2_14"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0158-6"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/948109.948149"},{"key":"e_1_2_1_62_1","unstructured":"Magnusson P. 2011. Understanding stacks and registers in the Sparc architecture(s). web.archive.org\/web\/20110610161119\/http:\/\/www.sics.se\/ psm\/sparcstack.html.  Magnusson P. 2011. Understanding stacks and registers in the Sparc architecture(s). web.archive.org\/web\/20110610161119\/http:\/\/www.sics.se\/ psm\/sparcstack.html."},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2150976.2151012"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_2"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.5555\/647171.718313"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1142980.1142985"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964029"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_5"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.5555\/22788.22800"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.5555\/1775223.1775241"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90091-1"},{"key":"e_1_2_1_73_1","doi-asserted-by":"crossref","unstructured":"Nielson F. and Nielson H. 1992. Two-level Functional Languages. Cambridge University Press.   Nielson F. and Nielson H. 1992. Two-level Functional Languages . Cambridge University Press.","DOI":"10.1017\/CBO9780511526572"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/309847.310101"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.5555\/647471.727270"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.5555\/645735.666115"},{"key":"e_1_2_1_77_1","unstructured":"PowerPC32. 2005. The PowerPC user instruction set architecture. doi.ieeecs.org\/10.1109\/MM.1994.363069.  PowerPC32. 2005. The PowerPC user instruction set architecture. doi.ieeecs.org\/10.1109\/MM.1994.363069."},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292553"},{"key":"e_1_2_1_79_1","unstructured":"Ramsey N. and Davidson J. 1999. Specifying instructions\u2019 semantics using \u03bb-RTL. http:\/\/www.cs.tufts.edu\/~nr\/pubs\/lrtl-tr.pdf  Ramsey N. and Davidson J. 1999. Specifying instructions\u2019 semantics using \u03bb -RTL. http:\/\/www.cs.tufts.edu\/~nr\/pubs\/lrtl-tr.pdf"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256225"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/1024393.1024410"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111542.1111560"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_6"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/1749608.1749613"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.009"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250750"},{"key":"e_1_2_1_88_1","unstructured":"Schmidt D. 1986. Denotational Semantics. Allyn and Bacon Boston MA.  Schmidt D. 1986. Denotational Semantics . Allyn and Bacon Boston MA."},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268950"},{"key":"e_1_2_1_90_1","unstructured":"Sharir M. and Pnueli A. 1981. Two approaches to interprocedural dataflow analysis. In Program Flow Analysis: Theory and Applications. Prentice-Hall.  Sharir M. and Pnueli A. 1981. Two approaches to interprocedural dataflow analysis. In Program Flow Analysis: Theory and Applications . Prentice-Hall."},{"key":"e_1_2_1_91_1","volume-title":"Computer Structures: Principles and Examples","author":"Siewiorek D.","year":"1982","unstructured":"Siewiorek , D. , Bell , G. , and Newell , A . 1982 . Computer Structures: Principles and Examples . Springer . Siewiorek, D., Bell, G., and Newell, A. 1982. Computer Structures: Principles and Examples. Springer."},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89862-7_1"},{"key":"e_1_2_1_93_1","volume-title":"SOOT: A Java optimization framework. www.sable.mcgill.ca\/soot\/.","author":"SOOT.","year":"2012","unstructured":"SOOT. 2012 . SOOT: A Java optimization framework. www.sable.mcgill.ca\/soot\/. SOOT. 2012. SOOT: A Java optimization framework. www.sable.mcgill.ca\/soot\/."},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.5555\/645867.670930"},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(93)90003-8"},{"key":"e_1_2_1_96_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_17"},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_10"},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_27"},{"key":"e_1_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.1145\/143095.143120"},{"key":"e_1_2_1_100_1","doi-asserted-by":"publisher","DOI":"10.1145\/73141.74819"},{"key":"e_1_2_1_101_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.129219"},{"key":"e_1_2_1_102_1","unstructured":"Wadler P. 1987. In The Implementation of Functional Programming Languages. Prentice-Hall Englewood Cliffs NJ 78--103.  Wadler P. 1987. In The Implementation of Functional Programming Languages . Prentice-Hall Englewood Cliffs NJ 78--103."},{"key":"e_1_2_1_103_1","unstructured":"WALA. 2006 WALA. wala.sourceforge.net\/wiki\/index.php\/.  WALA. 2006 WALA. wala.sourceforge.net\/wiki\/index.php\/."},{"key":"e_1_2_1_104_1","unstructured":"WALi 2007. WALi: The weighted automaton library. www.cs.wisc.edu\/wpis\/wpds\/download.php.  WALi 2007. WALi: The weighted automaton library. www.cs.wisc.edu\/wpis\/wpds\/download.php."},{"key":"e_1_2_1_105_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_8"},{"key":"e_1_2_1_106_1","volume-title":"Program Flow Analysis: Theory and Applications","author":"Wilhelm R.","unstructured":"Wilhelm , R. 1981. Global flow analysis and optimization in the MUG2 compiler generating system . In Program Flow Analysis: Theory and Applications . Prentice-Hall . Wilhelm, R. 1981. Global flow analysis and optimization in the MUG2 compiler generating system. In Program Flow Analysis: Theory and Applications. Prentice-Hall."},{"key":"e_1_2_1_107_1","doi-asserted-by":"publisher","DOI":"10.1145\/193209.193217"},{"key":"e_1_2_1_108_1","unstructured":"WPDS++ 2004. WPDS++: A C++ library for weighted pushdown systems. www.cs.wisc.edu\/wpis\/wpds\/download.php.  WPDS++ 2004. WPDS++: A C++ library for weighted pushdown systems. www.cs.wisc.edu\/wpis\/wpds\/download.php."},{"key":"e_1_2_1_109_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158642"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2450136.2450139","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2450136.2450139","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:18:49Z","timestamp":1750234729000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2450136.2450139"}},"subtitle":["A System for Generating Abstract Interpreters and its Application to Machine-Code Analysis"],"short-title":[],"issued":{"date-parts":[[2013,4]]},"references-count":108,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,4]]}},"alternative-id":["10.1145\/2450136.2450139"],"URL":"https:\/\/doi.org\/10.1145\/2450136.2450139","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,4]]},"assertion":[{"value":"2012-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-01-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-04-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}