Sound Modular Control-Flow Graph Extraction Tool
ConFlEx soundly extracts control flow graphs (CFG) from Java bytecode programs. The tool is written in OCAML. It uses Sawja/Javalib for manipulating Java class files, virtual method call resolution, and intermediate language (BIR) transformation. The extracted CFGs are suitable for the formal verification of control flow safety properties, such as in the CVPP project.