I participate on the CVPP project, which develops a Compositional Verification technique of control-flow safety properties. The verification principle has been implement into a tool set. Siavash Soleimanifard has developed ProMoVer tool, which, among other things, encapsulates the verification steps and provide to the user a unified view of the verification results. You can try the Promover on-line demo.
My role in CVPP is to research the extraction of models from software, to be used as input for the Model Checking step. Specifically, I research the extraction of Control-flow graphs from Java bytecode. The extraction follows formal rules, which are proven to soundly over-approximate the JVM behavior. I implement the rules in the ConFlEx tool, which is an original work of Afshin Amighi.
ConFlEx is control-flow graph (CFG) extractor from Java Bytecode. Currently it creates light-weight CFGs abstracting from all data, but preserving the branching structure, exceptions and method invocations. The tool is written in OCaml, and it uses the Sawja library, and its Bytecode Intermedia Representation (BIR) transformation to extract sound exceptional flow. The following poster gives a better understanding of ConFlEx approach (pdf). Currently I develop a modular framework for the sound extraction of CFGs from Java Bytecode. I plan to extend ConFlEx to extract CFGs modularly very soon.
I supervised Attilio Picoco in his Master thesis, named "Modular Extraction of Control-Flow graphs from Java Bytecode". October 2012. Attilio is also developer for ConFlEx.