ACM Transactions on Programming Languages and Systems · 2013 · 45 citations · 54 references
ComputingComputer ScienceFormal MethodsProgramming LanguagesSoftware EngineeringAbstract Syntax TreesDomain-specific LanguagesEvent RepresentationRuntime SystemsSoftware DesignSpecification LanguagesEvent-driven ProgrammingOperational SemanticsRuntime SemanticsStructural Operational Semantics
This article describes the design and implementation of a system, called T SL (for Transformer Specification Language), that provides a systematic solution to the problem of creating retargetable tools for analyzing machine code. T SL 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 T SL 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, T SL automatically creates the set of abstract transformers for the instructions of the instruction set. T SL 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. T SL is an abstract-transformer-generator generator . The article describes the principles behind T SL , and discusses how one uses T SL to develop different abstract interpreters.
54
Patrick Cousot, Radhia Cousot · 1977 · 6.2K citations
Patrice Godefroid, Nils Klarlund, Koushik Sen · ACM SIGPLAN Notices · 2005 · 2.1K citations
Systematic design of program analysis frameworks
Patrick Cousot, Radhia Cousot · 1979 · 1.6K citations · Full text