skip to main content
research-article
Open access

TSL: A System for Generating Abstract Interpreters and its Application to Machine-Code Analysis

Published: 01 April 2013 Publication History

Abstract

This article describes the design and implementation of a system, called TSL (for Transformer Specification Language), that provides a systematic solution to the problem of creating retargetable tools for analyzing machine code. TSL is a tool generator---that is, a metatool---that automatically creates different abstract interpreters for machine-code instruction sets.
The most challenging technical issue that we faced in designing TSL was how to automate the generation of the set of abstract transformers for a given abstract interpretation of a given instruction set. From a description of the concrete operational semantics of an instruction set, together with the datatypes and operations that define an abstract domain, TSL automatically creates the set of abstract transformers for the instructions of the instruction set. TSL 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.
TSL is an abstract-transformer-generator generator. The article describes the principles behind TSL, and discusses how one uses TSL to develop different abstract interpreters.

References

[1]
Alt, M. and Martin, F. 1995. Generation of efficient interprocedural analyzers with PAG. In Proceedings of the Statistical Analysis Symposium (SAS’95). Lecture Notes in Computer Science, vol. 983. Springer, 33--50.
[2]
Alur, R. and Madhusudan, P. 2006. Adding nesting structure to words. In Proceedings of the 10th International Conference on Developments in Language Theory (DLT’06). Lecture Notes in Computer Science, vol. 4036, Springer, 1--13.
[3]
APRON. 2007. APRON numerical abstract domain library. apron.cri.ensmp.fr.
[4]
ARMv7-A 2013. ARMv7-A in HOL. github.com/mn200/HOL/tree/master/examples/ARM/v7.
[5]
Assmann, U. 2000. Graph rewrite systems for program optimization. ACM Trans. Prog. Lang. Syst. 22, 4.
[6]
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.
[7]
Balakrishnan, G. and Reps, T. 2004. Analyzing memory accesses in x86 executables. In Proceedings of the International Conference on Compiler Construction (CC’04). 5--23.
[8]
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’07). 1--28.
[9]
Balakrishnan, G. and Reps, T. 2010. WYSINWYX: What you see is not what you execute. ACM Trans. Program. Lang. Syst. 32, 6.
[10]
Balakrishnan, G., Gruian, R., Reps, T., and Teitelbaum, T. 2005. Codesurfer/x86 - A platform for analyzing x86 executables, (tool demonstration paper). In Proceedings of the 14th International Conference on Compiler Construction (CC’05). 250--254.
[11]
Beckman, N., Nori, A., Rajamani, S., and Simmons, R. 2008. Proofs from tests. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA’08).
[12]
Bouajjani, A., Esparza, J., and Touili, T. 2003. A generic approach to the static analysis of concurrent programs with procedures. In Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 62--73.
[13]
Brauer, J. and King, A. 2012. Transfer function synthesis without quantiffer elimination. Logic. Methods Comput. Sci. 8, 3.
[14]
Brauer, J., King, A., and Kowalewski, S. 2012. Abstract interpretation of microcontroller code: Intervals meet congruences. Sci. Comput. Program. 77. To appear.
[15]
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’11).
[16]
Burstall, R. 1969. Proving properties of programs by structural induction. Comp. J. 12, 1, 41--48.
[17]
Cok, D. 2010. Safety in numbers. www.dtic.mil/dtic/tr/fulltext/u2/a532995.pdf.
[18]
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’93).
[19]
Cooper, K. and Kennedy, K. 1988. Interprocedural side-effect analysis in linear time. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. 57--66.
[20]
Cousot, P. 2003. Verification by abstract interpretation. In Proceedings of the International Symposium on Verification, Theory and Practice, Honoring Zohar Manna’s 64th Birthday. Lecture Notes in Computer Science, vol. 2772, Springer, 243--268.
[21]
Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 238--252.
[22]
Cousot, P. and Cousot, R. 1979. Systematic design of program analysis frameworks. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 269--282.
[23]
Cousot, P. and Cousot, R. 2000. Temporal abstract interpretation. In Proceedings of the 27th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 12--25.
[24]
Cousot, P. and Halbwachs, N. 1978. Automatic discovery of linear constraints among variables of a program. In Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 84--96.
[25]
Davidson, J. W. and Fraser, C. W. 1984. Code selection through object code optimization. ACM Trans. Program. Lang. Syst. 6, 4, 505--526.
[26]
de Moura, L. and Bjørner, 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.
[27]
Driscoll, E., Thakur, A., and Reps, T. 2012. OpenNWA: A nested-word-automaton library (tool paper). In Proceedings of the 24th International Conference on Computer Aided Verification. 665--671.
[28]
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.
[29]
Dutertre, B. and de Moura, L. 2006. Yices: An SMT solver. yices.csl.sri.com.
[30]
Elder, M., Lim, J., Sharma, T., Andersen, T., and Reps, T. 2011. Abstract domains of affine relations. In Proceedings of the 18th International Symposium on Static Analysis. Lecture Notes in Computer Science, vol. 6887, Springer, 198--215.
[31]
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.
[32]
Ferrante, J., Ottenstein, K., and Warren, J. 1987. The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst. 3, 9, 319--349.
[33]
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.
[34]
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.
[35]
Fox, A. and Myreen, M. 2010. A trustworthy monadic formalization of the ARMv7 instruction set architecture. In Proceedings of the International Conference on Interactive Theorem Proving. Lecture Notes in Computer Science, vol. 6172, Springer, 243--258.
[36]
Godefroid, P., Klarlund, N., and Sen, K. 2005. DART: Directed automated random testing. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’05). 213--223.
[37]
Graf, S. and Saïdi, H. 1997. Construction of abstract state graphs with PVS. In Proceedings of the 9th International Conference on Computer Aided Verification (CAV’97). Lecture Notes in Computer Science, vol. 1254, Springer, 72--83.
[38]
Gulavani, B., Henzinger, T., Kannan, Y., Nori, A., and Rajamani, S. 2006. SYNERGY: A new algorithm for property checking. In Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering. 117--127.
[39]
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.
[40]
IA32. 1999. Intel architecture software developer’s manual. developer.intel.com/design/pentiumii/manuals/243191.htm.
[41]
Intel. 2013a. Intel 64 and IA-32 architectures software developer’s manual, Vol. 2A: Instruction set reference, A-M. Intel. download.intel.com/design/processor/manuals/253666.pdf.
[42]
Intel. 2013b. Intel 64 and IA-32 architectures software developer’s manual, Vol. 2B: Instruction set reference, N-Z. Intel. download.intel.com/design/processor/manuals/253667.pdf.
[43]
Johnson, S. 1975. YACC: Yet another compiler-compiler. Tech. rep. 32, Bell Laboratories.
[44]
Jones, N., Gomard, C., and Sestoft, P. 1993. Partial Evaluation and Automatic Program Generation. Prentice-Hall International.
[45]
Jones, N. and Mycroft, A. 1986. Dataflow analysis of applicative programs using minimal function graphs. In Proceedings of the 13th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 296--306.
[46]
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.
[47]
Kästner, D. 2003. TDL: A hardware description language for retargetable postpass optimizations and analyses. In Proceedings of the 2nd International Conference on Generative Programming and Component Engineering (GPCE).
[48]
King, A. and Søndergaard, H. 2010. Automatic abstraction for congruences. In Proceedings of the 11th International Conference on Verification, Model Checking, and Abstract Interpretation. 197--213.
[49]
Kodumal, J. and Aiken, A. 2005. Banshee: A scalable constraint-based analysis toolkit. In Proceedings of the 12th International Symposium on Static Analysis (SAS’05). Lecture Notes in Computer Science, vol. 3672, Springer, 218--234.
[50]
Lacey, D., Jones, N., Van Wyk, E., and Frederiksen, C. 2004. Compiler optimization correctness by temporal logic. Higher-Order Symbol. Comput. 17, 3.
[51]
Lal, A. and Reps, T. 2006. Improving pushdown system model checking. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV’06). 343--357.
[52]
Lal, A., Reps, T., and Balakrishnan, G. 2005. Extended weighted pushdown systems. In Proceedings of the 17th International Conference on Computer Aided Verification (CAV’05). 434--448.
[53]
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.
[54]
Lattner, C. and Adve, V. 2004. LLVM: A compilation framework for lifelong program analysis and transformation. In International Symposium on Code Generation and Optimization.
[55]
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’00). 280--301.
[56]
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.
[57]
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.
[58]
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.
[59]
Lim, J., Lal, A., and Reps, T. 2009. Symbolic analysis via semantic reinterpretation. In Proceedings of the 16th International SPIN Workshop.
[60]
Lim, J., Lal, A., and Reps, T. 2011. Symbolic analysis via semantic reinterpretation. Softw. Tools Tech. Transfer 13, 1, 61--87.
[61]
Linn, C. and Debray, S. 2003. Obfuscation of executable code to improve resistance to static disassembly. In Proceedings of the 10th ACM Conference on Computer and Communications Security (CCS’03). 290--299.
[62]
Magnusson, P. 2011. Understanding stacks and registers in the Sparc architecture(s). web.archive.org/web/20110610161119/http://www.sics.se/ psm/sparcstack.html.
[63]
Malmkjær, K. 1993. Abstract interpretation of partial-evaluation algorithms. Ph.D. thesis, Department of Computer and Information Science, Kansas State University.
[64]
Martignoni, L., McCamant, S., Poosankam, P., Song, D., and Maniatis, P. 2012. Path-Exploration lifting: Hi-fi tests for lo-fi emulators. In Proceedings of the 17th International Conference on Architectural Support for Programming Languages and Operating Systems. 337--348.
[65]
Mauborgne, L. and Rival, X. 2005. Trace partitioning in abstract interpretation based static analyzers. In Proceedings of the European Symposium on Programming (ESOP’05). Lecture Notes in Computer Science, vol. 3444, Springer, 5--20.
[66]
Miné, A. 2002. A few graph-based relational numerical abstract domains. In Proceedings of the 9th International Symposium on Static Analysis (SAS’02). Lecture Notes in Computer Science, vol. 2477, Springer, 117--132.
[67]
Mishra, P., Shrivastava, A., and Dutt, N. 2006. Architecture description language: Driven software toolkit generation for architectural exploration of programmable socs. ACM Trans. Design Autom. Electron. Syst. 11, 3, 626--658.
[68]
Müller-Olm, M. and Seidl, H. 2004. Precise interprocedural analysis through linear algebra. In Proceedings of the ACM Symposium on Principles of Programming Languages.
[69]
Müller-Olm, M. and Seidl, H. 2005. Analysis of modular arithmetic. In Proceedings of the 14th European Symposium on Programming (ESOP’05). Lecture Notes in Computer Science, vol. 3444, Springer, 46--60.
[70]
Mycroft, A. and Jones, N. 1985. A relational framework for abstract interpretation. In Proceedings of the Workshop on Programs as Data Objects. Lecture Notes in Computer Science, vol. 217, Springer, 156--171
[71]
Myreen, M., Fox, A., and Gordon, M. 2007. Hoare logic for ARM machine code. In Proceedings of the International Symposium on Fundamentals of Software Engineering. Lecture Notes in Computer Science, vol. 4767, Springer, 272--286.
[72]
Nielson, F. 1989. Two-level semantics and abstract interpretation. Theor. Comput. Sci. 69, 117--242.
[73]
Nielson, F. and Nielson, H. 1992. Two-level Functional Languages. Cambridge University Press.
[74]
Pees, S., Hoffmann, A., Zivojnovic, V., and Meyr, H. 1999. LISA machine description language for cycle-accurate models of programmable DSP architectures. In Proceedings of the 36th Annual ACM/IEEE Design Automation Conference (DAC’99). 933--938.
[75]
Pettersson, M. 1992. A term pattern-match compiler inspired by finite automata theory. In Proceedings of the 4th International Conference on Compiler Construction (CC’92). 258--270.
[76]
Pleban, U. and Lee, P. 1987. High-level semantics. In Proceedings of the 3rd Workshop on Mathematical Foundations of Programming Language Semantics. Lecture Notes in Computer Science, vol. 298, Springer, 550--571.
[77]
PowerPC32. 2005. The PowerPC user instruction set architecture. doi.ieeecs.org/10.1109/MM.1994.363069.
[78]
Ramalingam, G., Field, J., and Tip, F. 1999. Aggregate structure identification and its application to program analysis. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’99). 119--132.
[79]
Ramsey, N. and Davidson, J. 1999. Specifying instructions’ semantics using λ-RTL. http://www.cs.tufts.edu/~nr/pubs/lrtl-tr.pdf
[80]
Ramsey, N. and Fernández, M. 1997. Specifying representations of machine instructions. ACM Trans. Program. Lang. Syst. 19, 3, 492--524.
[81]
Regehr, J. and Reid, A. 2004. HOIST: A system for automatically deriving static analyzers for embedded systems. In Proceedings of the 11th International Conference on Architectural Support for Programming Languages and Operating Systems. 133--143.
[82]
Reps, T., Balakrishnan, G., and Lim, J. 2006. Intermediate-representation recovery from low- level code. In Workshop on Partial Evaluation and Semantics-Based Program Manipulation.
[83]
Reps, T., Lim, J., Thakur, A., Balakrishnan, G., and Lal, A. 2010a. There’s plenty of room at the bottom: Analyzing and verifying machine code. In Proceedings of the 22nd International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 6174, Springer, 41--56.
[84]
Reps, T., Sagiv, M., and Loginov, A. 2010b. Finite differencing of logical formulas for static analysis. ACM Trans. Program. Lang. Syst. 6, 32.
[85]
Reps, T., Sagiv, M., and Yorsh, G. 2004. Symbolic implementation of the best transformer. In Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI’04). Lecture Notes in Computer Science, vol. 4349, Springer, 252--266.
[86]
Reps, T., Schwoon, S., Jha, S., and Melski, D. 2005. Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program. 58, 1--2, 206--263.
[87]
Scherpelz, E., Lerner, S., and Chambers, C. 2007. Automatic inference of optimizer flow functions from semantics meanings. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’07). 135--145.
[88]
Schmidt, D. 1986. Denotational Semantics. Allyn and Bacon, Boston, MA.
[89]
Schmidt, D. 1998. Dataflow analysis is model checking of abstract interpretations. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 38--48.
[90]
Sharir, M. and Pnueli, A. 1981. Two approaches to interprocedural dataflow analysis. In Program Flow Analysis: Theory and Applications. Prentice-Hall.
[91]
Siewiorek, D., Bell, G., and Newell, A. 1982. Computer Structures: Principles and Examples. Springer.
[92]
Song, D., Brumley, D., Yin, H., Caballero, J., Jager, I., Kang, M., Liang, Z., Newsome, J., Poosankam, P., and Saxena, P. 2008. BitBlaze: A new approach to computer security via binary analysis. In Proceedings of the 4th International Conference on Information Systems Security (ICISS’08). Lecture Notes in Computer Science, vol. 5352, 1--25.
[93]
SOOT. 2012. SOOT: A Java optimization framework. www.sable.mcgill.ca/soot/.
[94]
Steffen, B. 1991. Dataflow analysis as model checking. In Proceedings of the International Conference on Theoretical Aspects of Computer Software (TACS’91). Lecture Notes in Computer Science, vol. 526, Springer, 346--365.
[95]
Steffen, B. 1993. Generating dataflow analysis algorithms from modal specifications. Sci. Comput. Program. 21, 2, 11--139.
[96]
Thakur, A. and Reps, T. 2012. A method for symbolic computation of abstract operations. In Proceedings of the 24nd International Conference on Computer Aided Verification (CAV’12). Lecture Notes in Computer Science, vol. 7358, Springer, 174--192.
[97]
Thakur, A., Elder, M., and Reps, T. 2012. Bilateral algorithms for symbolic abstraction. In Proceedings of the 19th International Symposium on Static Analysis. Lecture Notes in Computer Science, vol. 7460, Springer, 111--128
[98]
Thakur, A., Lim, J., Lal, A., Burton, A., Driscoll, E., Elder, M., Andersen, T., and Reps, T. 2010. Directed proof generation for machine code. In Proceedings of the 22nd International Conference on Computer Aided Verification (CAV’10). Lecture Notes in Computer Science, vol. 6174, Springer, 288--305.
[99]
Tjiang, S. and Hennessy, J. 1992. Sharlit: A tool for building optimizers. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’92). 82--93.
[100]
Venkatesh, G. 1989. A framework for construction and evaluation of high-level specifications for program analysis techniques. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’89). 1--12.
[101]
Venkatesh, G. and Fischer, C. 1992. SPARE: A development environment for program analysis algorithms. Trans. Softw. Engin. 18, 4.
[102]
Wadler, P. 1987. In The Implementation of Functional Programming Languages. Prentice-Hall, Englewood Cliffs, NJ, 78--103.
[103]
WALA. 2006 WALA. wala.sourceforge.net/wiki/index.php/.
[104]
WALi 2007. WALi: The weighted automaton library. www.cs.wisc.edu/wpis/wpds/download.php.
[105]
Whaley, J., Avots, D., Carbin, M., and Lam, M. 2005. Using Datalog with binary decision diagrams for program analysis. In Proceedings of the 3rd Asian Symposium on Programming Languages and Systems. Lecture Notes in Computer Science, vol. 3780, Springer, 97--118.
[106]
Wilhelm, R. 1981. Global flow analysis and optimization in the MUG2 compiler generating system. In Program Flow Analysis: Theory and Applications. Prentice-Hall.
[107]
Wilson, R., French, R., Wilson, C., Amarasinghe, S., Anderson, J.-A., Tjiang, S., Liao, S.-W., Tseng, C.-W., Hall, M., Lam, M., and Hennessy, J. 1994. SUIF: An infrastructure for research on parallelizing and optimizing compilers. SIGPLAN Not. 29, 12.
[108]
WPDS++ 2004. WPDS++: A C++ library for weighted pushdown systems. www.cs.wisc.edu/wpis/wpds/download.php.
[109]
Yi, K. and Harrison III, W. 1993. Automatic generation and management of interprocedural program analyses. In Proceedings of the 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’93). 246--259.

Cited By

View all
  • (2024)Synthesizing Formal Semantics from Executable InterpretersProceedings of the ACM on Programming Languages10.1145/36897248:OOPSLA2(362-388)Online publication date: 8-Oct-2024
  • (2024)libLISA: Instruction Discovery and Analysis on x86-64Proceedings of the ACM on Programming Languages10.1145/36897238:OOPSLA2(333-361)Online publication date: 8-Oct-2024
  • (2023)Deriving Abstract Interpreters from Skeletal SemanticsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.387.8387(97-113)Online publication date: 14-Sep-2023
  • Show More Cited By

Index Terms

  1. TSL: A System for Generating Abstract Interpreters and its Application to Machine-Code Analysis

                              Recommendations

                              Comments

                              Information & Contributors

                              Information

                              Published In

                              cover image ACM Transactions on Programming Languages and Systems
                              ACM Transactions on Programming Languages and Systems  Volume 35, Issue 1
                              April 2013
                              240 pages
                              ISSN:0164-0925
                              EISSN:1558-4593
                              DOI:10.1145/2450136
                              Issue’s Table of Contents
                              Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

                              Publisher

                              Association for Computing Machinery

                              New York, NY, United States

                              Publication History

                              Published: 01 April 2013
                              Accepted: 01 January 2013
                              Revised: 01 January 2013
                              Received: 01 October 2012
                              Published in TOPLAS Volume 35, Issue 1

                              Permissions

                              Request permissions for this article.

                              Check for updates

                              Author Tags

                              1. Abstract interpretation
                              2. dataflow analysis
                              3. dynamic analysis
                              4. machine-code analysis
                              5. static analysis
                              6. symbolic analysis

                              Qualifiers

                              • Research-article
                              • Research
                              • Refereed

                              Funding Sources

                              Contributors

                              Other Metrics

                              Bibliometrics & Citations

                              Bibliometrics

                              Article Metrics

                              • Downloads (Last 12 months)244
                              • Downloads (Last 6 weeks)23
                              Reflects downloads up to 14 Feb 2025

                              Other Metrics

                              Citations

                              Cited By

                              View all
                              • (2024)Synthesizing Formal Semantics from Executable InterpretersProceedings of the ACM on Programming Languages10.1145/36897248:OOPSLA2(362-388)Online publication date: 8-Oct-2024
                              • (2024)libLISA: Instruction Discovery and Analysis on x86-64Proceedings of the ACM on Programming Languages10.1145/36897238:OOPSLA2(333-361)Online publication date: 8-Oct-2024
                              • (2023)Deriving Abstract Interpreters from Skeletal SemanticsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.387.8387(97-113)Online publication date: 14-Sep-2023
                              • (2022)Towards a Semantic-Aware Code Generator for Cyber-Physical Systems2022 11th Mediterranean Conference on Embedded Computing (MECO)10.1109/MECO55406.2022.9797167(1-6)Online publication date: 7-Jun-2022
                              • (2021)Program analysis via efficient symbolic abstractionProceedings of the ACM on Programming Languages10.1145/34854955:OOPSLA(1-32)Online publication date: 15-Oct-2021
                              • (2021)An Isabelle/HOL Formalisation of the SPARC Instruction Set Architecture and the TSO Memory ModelJournal of Automated Reasoning10.1007/s10817-020-09579-465:4(569-598)Online publication date: 1-Apr-2021
                              • (2019)A complete formal semantics of x86-64 user-level instruction set architectureProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314601(1133-1148)Online publication date: 8-Jun-2019
                              • (2019)ISA semantics for ARMv8-a, RISC-v, and CHERI-MIPSProceedings of the ACM on Programming Languages10.1145/32903843:POPL(1-31)Online publication date: 2-Jan-2019
                              • (2018)Do Students' Learning Behaviors Differ when they Collaborate in Open-Ended Learning Environments?Proceedings of the ACM on Human-Computer Interaction10.1145/32743182:CSCW(1-19)Online publication date: 1-Nov-2018
                              • (2018)A new abstraction framework for affine transformersFormal Methods in System Design10.1007/s10703-018-0325-zOnline publication date: 18-Oct-2018
                              • Show More Cited By

                              View Options

                              View options

                              PDF

                              View or Download as a PDF file.

                              PDF

                              eReader

                              View online with eReader.

                              eReader

                              Login options

                              Full Access

                              Figures

                              Tables

                              Media

                              Share

                              Share

                              Share this Publication link

                              Share on social media