ConFlEx - Sound Modular Control-Flow Graph Extraction ToolThe ConFlEx tool aims to extract soundly the control-flow graphs from Java bytecode programs. The tool is written in OCAML, and uses Sawja/Javalib, a set of libraries from Inria/Rennes to manipulate Java class files, virtual method call resolution, and transformation into an intermediate stackless-language (BIR). The goal of the tool is to produce suitable models for the formal verification of control-flow safety properties. That is, we are concerned to the correctness of our extraction algorithm, and the type of properties that it preserves. Thus, together with the tool, we are interested in theoretical results that show the property preservation. Following is the code for ConFlEx, and the customized version of Sawja. There is a rudimentary README inside the files, which explain the installation procedure. In case you have any trouble in the installation process, don't exhitate to contact the authors: - conflex-0.2.tar.bz2 - sawja-1.3.tar.bz2 You can also try a non-modular version of ConFlEx on-line. |
Last Modified: June 25 2013.