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 lor intraprocedural data-flow analysis via model chocking. 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 clogantly provides a fully integrated implementation of Data-Flow Analysis as Model Checking in a software development environment;. © Springer-Vellag Berlin Fleidelberg 2006.
Cite
CITATION STYLE
Lampreclit, A. L., Margaria, T., & Steffen, B. (2006). Data-Flow Analysis as Model Checking within the jABC. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3923 LNCS, pp. 101–104). https://doi.org/10.1007/11688839_9
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
