Bounded Model Checking of Embedded Software in Wireless Cognitive Radio Systems

We present a new verification approach that applies aggressive program slicing and a proof-based abstraction-refinement strategy to enhance the scalability of bounded model checking of embedded software. nile many software model-checking tools use program slicing as a separate or optional step, our program slicing is integrated in the model construction and reduction process. And it is combined with the compilation optimization techniques so to compute a more accurate slice. We also explore a proof-based abstraction-refinement strategy using the under/over-approximation on our proposed software model, and propose a heuristic method of deciding new encoding size to refine the under-approximation. Experiments on C programs from wireless cognitive radio systems show this approach can greatly reduce the model size and shorten the solving time by the SA T-solver.