Using Runtime Analysis To Guide Model Checking of Java Programs

This paper takes the Eraser algorithm which detects data races in a program by studying a single run of the program and from that trying to conclude whether any runs with data races are possible.

This was implemented in JPF2 and it can be run Eraser mode. This is implemented specifically to see if there are unprotected variables. This can yield in lots of warnings that are not valid.

For our research, combined with static analysis, a few runs of the programs are done. Relevant data is collected. If there is user input we should test the boundary values in a finite system. And some random values. Mark the critical points in the program and see if the values at those points change drastically or not? If they do change drastically then see what is causing it? Whether it is system stuff or whether it is user stuff or even random? This could help us detect where the major fluctuations occur in the program. This information can be used to guide the heuristic alongwith the static anaylsis. Ideally this information should lie on top of the control flow graph.