TY - GEN
T1 - Data-Flow Analysis as Model Checking within the jABC
AU - Lampreclit, Anna Lena
AU - Margaria, Tiziana
AU - Steffen, Bernhard
PY - 2006
Y1 - 2006
N2 - 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;.
AB - 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;.
UR - http://www.scopus.com/inward/record.url?scp=33745797496&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:33745797496
SN - 354033050X
SN - 9783540330509
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 101
EP - 104
BT - Compiler Construction - 15th International Conference, CC 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Proceedings
T2 - 15th International Conference on Compiler Construction, CC 2006. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006
Y2 - 30 March 2006 through 31 March 2006
ER -