Data-flow analysis as model checking within the jABC
2006 | conference paper. A publication with affiliation to the University of Göttingen.
Jump to: Cite & Linked | Documents & Media | Details | Version history
Documents & Media
Details
- Authors
- Lamprecht, Anna-Lena; Margaria, Tiziana ; Steffen, Bernhard
- Editors
- Mycroft, Alan; Zeller, Andrea
- 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.
- Issue Date
- 2006
- Publisher
- Springer
- Conference
- 15th International Conference on Compiler Construction
- Series
- Lecture Notes in Computer Science
- ISBN
- 3-540-33050-X
978-3-540-33050-9 - Conference Place
- Vienna
- Event start
- 2006-03-30
- Event end
- 2006-03-31
- ISSN
- 0302-9743
- Language
- English