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. While 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/overapproximation 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 SAT-solver.