PAG

PAG -- an efficient program analyzer generator. In order to produce high quality code, compilers have to perform efficiency increasing program transformations. These transformations usually depend on preceding program analyses. These analyses, known a data flow analyses or abtract interpretations, may range from “simple” intraprocedural bit vector frameworks to very complex inteprocedural alias analyses. Their implementation may be difficult and expensive. By exploiting the underlying theories of abstract interpretation and data flow analysis the implementation and design of analyzers can be supported by a tool. Abstract interpretation provides the relation to the semantics of the language and allows the systematic derivation of provably correct and terminating analyses. Data flow analysis supplies many efficient algorithms, such as fixed point iterations. The program analyzer generator PAG described in the paper attempts to offer the best of both worlds, specification languages based on the clean theory of abstract interpretation and efficient implementation methods from the theory of data flow analysis. PAG has a high level functional input language to specify data flow analyses. It offers the generation of complex data structures and is therefore not limited to bit vector problems. PAG generated interprocedural analyzers can be easily integrated into existing compilers. PAG has successuflly been used in the ESPRIT project COMPARE to generate several analyzers (including alias analysis and constant propagation) for industrial quality ANSI-C and Fortran90 compilers, and is now marketed by the spin-off company AbsInt. A simplified version of PAG can be interactively tested over the Web.


References in zbMATH (referenced in 21 articles , 1 standard article )

Showing results 1 to 20 of 21.
Sorted by year (citations)

1 2 next

  1. Prantl, Adrian; Schordan, Markus; Knoop, Jens: Tubound -- a conceptually new tool for worst-case execution time analysis (2008)
  2. Beyer, Dirk; Henzinger, Thomas A.; Théoduloz, Grégory: Configurable software verification: Concretizing the convergence of model checking and program analysis (2007)
  3. Eo, Hyunjun; Yi, Kwangkeun; Choe, Kwang-Moo: Static extensivity analysis for $\lambda$-definable functions over lattices (2006)
  4. Zeng, Jia; Mitchell, Chuck; Edwards, Stephen A.: A domain-specific language for generating dataflow analyzers. (2006)
  5. Ferré, Sébastien; King, Ross D.: A dichotomic search algorithm for mining and learning in domain-specific logics (2005)
  6. Meyerhöfer, Marcus; Meyer-Wegener, Klaus: Estimating non-functional properties of component-based software based on resource consumption. (2005)
  7. Salcianu, Alexandru; Arkoudas, Konstantine: Machine-checkable correctness proofs for intra-procedural dataflow analyses. (2005)
  8. Coors, Martin; Keding, Holger; Lüthje, Olaf; Meyr, Heinrich: Design and DSP implementation of fixed-point systems (2002)
  9. Evstiougov-Babaev, Alexander A.: Call graph and control flow graph visualization for developers of embedded applications (2002)
  10. Ferré, Sébastien; Ridoux, Olivier: A framework for developing embeddable customized logics (2002)
  11. Manevich, R.; Ramalingam, G.; Field, J.; Goyal, D.; Sagiv, M.: Compactly representing first-order structures for static analysis (2002)
  12. Probst, Christian W.: Modular control flow analysis for libraries (2002)
  13. Ruf, Erik: Improving the precision of equality-based dataflow analyses (2002)
  14. Adve, Vikram; Sakellariou, Rizos: Compiler synthesis of task graphs for parallel program performance prediction (2001)
  15. Ferdinand, Christian; Heckmann, Reinhold; Langenbach, Marc; Martin, Florian; Schmidt, Michael; Theiling, Henrik; Thesing, Stephan; Wilhelm, Reinhard: Reliable and precise WCET determination for a real-life processor (2001)
  16. Guyer, Samuel Z.; Lin, Calvin: Optimizing the use of high performance software libraries (2001)
  17. Leupers, Rainer: Code optimization techniques for embedded processors. Methods, algorithms, and tools (2000)
  18. Ferdinand, Christian; Martin, Florian; Wilhelm, Reinhard; Alt, Martin: Cache behavior prediction by abstract interpretation (1999)
  19. Fecht, Christian; Seidl, Helmut: Propagating differences: An efficient new fixpoint algorithm for distributive constraint systems (1998)
  20. Martin, Florian: PAG -- an efficient program analyzer generator (1998)

1 2 next