Advertisement

An Algebraic Approach to the Static Analysis of Concurrent Software

  • Javier Esparza
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2477)

Abstract

In the last years a group of colleagues and I have developed a new approach to interprocedural program analysis based on ideas born in the model-checking community [2,3,4,6]. The Moped tool [8] is an implementation of most of this work. In interaction with the SLAM toolkit [1], Moped has been applied to the analysis of programs with thousands of lines of C code.

References

  1. 1.
    T. Ball and S. Rajamani: The SLAM Project: Debugging System Software via Static Analysis Conference Record of POPL’ 02, 1–3, ACM Press (2002).Google Scholar
  2. 2.
    A. Bouajjani, J. Esparza and O. Maler: Reachability Analysis of Pushdown Automata: Application to Model-Checking. Proceedings of CONCUR’ 97, LNCS 1243, 135–150 (1997).Google Scholar
  3. 3.
    J. Esparza, D. Hansel, P. Rossmanith and S. Schwoon: Efficient Model Checking Algorithms for Pushdown Systems. Proceedings of CAV’ 00, LNCS 1855, 232–247 (2000).Google Scholar
  4. 4.
    J. Esparza and J. Knoop: An Automata-theoretic Approach to Interprocedural Dataflow Analysis. Proceedings of FOSSACS’ 99, LNCS 1578, 14–30 (1999).Google Scholar
  5. 5.
    J. Esparza and A. Podelski: Efficient algorithms for pre* and post* on Interprocedural Parallel Flow Graphs. Conference Record of POPL’ 00, 1–11, ACM Press (2000).Google Scholar
  6. 6.
    J. Esparza and S. Schwoon: A BBD-Based Model Checker for Recursive Programs. Proceedings of CAV’ 01, LNCS 2102, 324–336 (2001).Google Scholar
  7. 7.
    M.W. Hopkins and D.C. Kozen: Parikh’s Theorem in Commutative Kleene Algebra Proceedings of LICS’99, IEEE, 394–401 (1999)Google Scholar
  8. 8.
    Moped-A Model-Checker for Pushdown Systems. Writen and maintained by Stefan Schwoon. Code available at http://www7.in.tum.de~schwoon/moped.

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Javier Esparza
    • 1
  1. 1.Laboratory for Foundations of Computer ScienceUniversity of EdinburghGermany

Personalised recommendations