Early Results with Precision Abstraction: Using Data-flow Analysis to Improve the Scalability of Model Checking

This paper presents a new state space reduction technique that applies to model checking of software. The new technique, precision abstraction, borrows ideas from dataflow analysis to identify procedures that can be analyzed context-insensitively without affecting the accuracy of the verification of a given property. These context-insensitive procedures can then be represented with fewer states than would be needed context-sensitive analysis. Preliminary results indicate that the number of transitions in the analysis prescribed by our approach is at least 155 times fewer than the exhaustive analysis a model checker would otherwise perform.