Ant Colony Optimization directed program abstraction for software bounded model checking

The increasing complexity and size of software designs has made scalability a major bottleneck in software verification. Program abstraction has shown potential in alleviating this problem through selective search space reduction. In this paper, we propose an Ant Colony Optimization (ACO)-directed program structure construction to formulate a novel under-approximation based program abstraction (UAPA). By taking advantage of the resulting abstraction, a new software bounded model checking framework is built with the aim of improving the performance of property checking, especially for property falsification. Experimental results on various programs showed that the proposed ACO-directed program abstraction can dramatically improve the performance of software bounded model checking with significant speedups.