If you haven’t already, install the PCG Toolbox plugin into Eclipse.

Projected Control Graph (PCG) is an abstraction to derive relevant behaviors in a given program. PCG has numerous applications in program comprehension, analysis, and verification. The PCG toolbox provides tools to compute and visualize PCGs. It supports analysis of C code, Java source code and Java Byte Code (Jimple). It is implemented as a eclipse plugin using Atlas, a graphical program analysis platform. Atlas facilitates creation of graphical abstractions to analyze programs and thus before you could use the toolbox, you will need to ‘index’ your application into Atlas. The steps to do that are documented here.

Video Tutorial

A detailed description of how to use the toolbox to compute PCGs and how to use them to verify safety properties of a software is provided in the following video.