In this project, we are trying to bridge two verification tools Jahob and Armc. Jahob is quite powerful in accepting complecated Java programs and translate it into simplified intermidiate language. We are trying to write a translater from this representation of program to input format of ARMC. ARMC takes transition relation as input. ARMC is powerful in computing loop invariant and fixedpoint analysis automaticlly. Result of ARMC can be fed back to Jahob to improe its analysis of programs. (Both the tools are evolving and It is difficult to claim about their capabilities.)

I am going to present following paper which describes internal functions of ARMC.

ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement