An Algebraic Approach to the Static Analysis of Concurrent Software
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  is an implementation of most of this work. In interaction with the SLAM toolkit , Moped has been applied to the analysis of programs with thousands of lines of C code.
- 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.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.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.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.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.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.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.Moped-A Model-Checker for Pushdown Systems. Writen and maintained by Stefan Schwoon. Code available at http://www7.in.tum.de~schwoon/moped.