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

ARMC stands for Abstract Refinement Model Checker. We have already learned this methodlogy in the course. This model checker executes program using abstract set of states. Model checker divided its process in following three procedures:

1. Abstract Fixed Point
2. Feasible Counter Example
3. Refine

ARMC calls them in a loop. Until any of the following two event happens:

1. Abstract Fixed Point finds a fixed point which does not contain error state.
2. Feasible Counter Example finds a concrete counter example.