Static Analysis for Model Checking

Here are some must read before doing any kind of Static Analysis in Model Checking. This is mostly structural based static analysis. Most everything I have found is in the Java PathFinder. Nobody seems to have done it with Murphi or SPIN. I guess the way Murphi and SPIN are designed, it would really hard to do similar kind of things.

1. Byte Code Distance Heuristics and Trail Direction for Model Checking Java Programs
by Stefan Edelkamp and Tilman Mehler

-- cite this paper for FSM

2. Heuristic Model Checking for Java Programs
by Alex Groce and W. Visser

-- this paper has the interleaving thread stuff

3. Combining Static Analysis and Model Checking for Software Analysis
by G.Brat and W. Visser

-- cite this paper for on-demand heuristic

4. Model Checking Java Programs using Structural Heuristic
by A Groce and W. Visser

-- cite this paper as an example of structural heuristic