bild
School of
Computer Science
and Communication
KTH / CSC / TCS / People / Pedro

Academic Research

CVPP is a project to develop a Compositional Verification technique of control-flow safety properties. The verification framework has been implement into a tool set with the same name. 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's 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. 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 Intermediate Representation (BIR) transformation to extract sound exceptional flow. The following poster gives a better understanding of ConFlEx approach (pdf). The tool has been extended by me and Attilio Picoco to be able to extract modularly CFGs from incomplete Java Bytecode programs, using user-provided interfaces. I supervised Attilio in his Master thesis, named Modular Extraction of Control-Flow graphs from Java Bytecode" (October 2012). Currently I develop a modular framework for the sound extraction of CFGs from Java Bytecode.

STaVe is a tool to specify and prove the correct usage of condition variables (CVs). STaVe extracts synchronization schemes from the annotated Java source program as a SyncTask, a simple non-procedural imperative language to specify synchronization schemes using CVs. Then, STaVe converts SyncTask programs into Coloured Petri Nets (CPNs), and prove the correct synchronization using a CPN analysis tool. Currently it supports only the CPN Tools format, but the output to other formats are on the wishlist. The theoretical results behind the STaVe approach are to appear.

Last Modified: June 18 2015.