Data-flow analysis as model checking within the jABC

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 p-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.