Abstract
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.
Chapter PDF
Similar content being viewed by others
References
Aho, A., Ullman, J.: Principles of Compiler Design, vol. 3. Addison-Wesley, Reading (1979)
Clarke, E., Grumberg, O., Peled, D.: Model Checking, vol. 3. MIT Press, Cambridge (2001)
Hecht, M.: Flow Analysis of Computer Programs. Programming Languages Ser., vol. 5. Elsevier Science Ltd, Amsterdam (1977)
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)
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)
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)
Nagel, R.: Java abc framework (July 2005), http://jabc.cs.uni-dortmund.de
Nielson, F., Nielson, H., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)
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)
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)
Steffen, B.: Generating data flow analysis algorithms from modal specifications. Sci. Comput. Program. 21(2), 115–139 (1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lamprecht, AL., Margaria, T., Steffen, B. (2006). Data-Flow Analysis as Model Checking Within the jABC. In: Mycroft, A., Zeller, A. (eds) Compiler Construction. CC 2006. Lecture Notes in Computer Science, vol 3923. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11688839_9
Download citation
DOI: https://doi.org/10.1007/11688839_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33050-9
Online ISBN: 978-3-540-33051-6
eBook Packages: Computer ScienceComputer Science (R0)