Data-Flow Analysis as Model Checking Within the jABC

  • Anna-Lena Lamprecht
  • Tiziana Margaria
  • Bernhard Steffen
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3923)


This paper describes how the jABC, a generic framework for library-based program development, and two of its plugins - the Model Checker and a flow graph converter – form a framework for intraprocedural data-flow analysis via model checking. Based on functionalities provided by the Soot program analysis platform, the converter generates graph structures from Java classes. Data flow analyses are then expressed as formulas in the modal μ-calculus. Executing the analysis is carried out by checking the validity of the formulas on the flow graph.

The tool demonstration will illustrate the interplay of the involved components, which elegantly provides a fully integrated implementation of Data-Flow Analysis as Model Checking in a software development environment.


  1. 1.
    Aho, A., Ullman, J.: Principles of Compiler Design, vol. 3. Addison-Wesley, Reading (1979)zbMATHGoogle Scholar
  2. 2.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking, vol. 3. MIT Press, Cambridge (2001)Google Scholar
  3. 3.
    Hecht, M.: Flow Analysis of Computer Programs. Programming Languages Ser., vol. 5. Elsevier Science Ltd, Amsterdam (1977)zbMATHGoogle Scholar
  4. 4.
    Margaria, T.: Components, features, and agents in the abc. In: Ryan, M.D., Meyer, J.-J.C., Ehrich, H.-D. (eds.) Dagstuhl Seminar 2003. LNCS, vol. 2975, pp. 154–174. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Margaria, T., Nagel, R., Steffen, B.: jeti: A tool for remote tool integration. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 557–562. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Müller-Olm, M., Schmidt, D., Steffen, B.: Model-checking: A tutorial introduction. In: Cortesi, A., Filé, G. (eds.) SAS 1999. LNCS, vol. 1694, pp. 330–354. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  7. 7.
    Nagel, R.: Java abc framework (July 2005),
  8. 8.
    Nielson, F., Nielson, H., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)CrossRefzbMATHGoogle Scholar
  9. 9.
    Schmidt, D., Steffen, B.: Program analysis as model checking of abstract interpretations. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 351–380. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  10. 10.
    Steffen, B.: Data flow analysis as model checking. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 346–365. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  11. 11.
    Steffen, B.: Generating data flow analysis algorithms from modal specifications. Sci. Comput. Program. 21(2), 115–139 (1993)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2006

Authors and Affiliations

  • Anna-Lena Lamprecht
    • 1
  • Tiziana Margaria
    • 1
  • Bernhard Steffen
    • 2
  1. 1.Service Engineering for Distributed SystemsUniversität GöttingenGermany
  2. 2.Chair of Programming SystemsUniversität DortmundGermany

Personalised recommendations