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.

1. Infrastructure for ARMC translation is done.
2. Able to translate simple arithmetic programs.
3. De-sugaring of program calls yet to be done.
4. Only very simple formula can be processed.( Need to convert Formula to DNF form)
5. Sometimes generates buggy transition relation ( But few tests are working well. )
6. Support for If and Loops is incomplete.

1. It took some time to understand Jahob data-structures.
2. Some places it was difficult to say what format of formula program will receive.
3. Needs more experimentation and effort.