Efficient SAT-based bounded model checking for software verification

摘要

This paper discusses our methodology for formal analysis and automatic verification of software programs. It is applicable to a large subset of the C programming language that includes pointer arithmetic and bounded recursion. We consider reachability properties, in particular whether certain assertions or basic blocks are reachable in the source code, or whether certain standard property violations can occur. We perform this analysis via a translation to a Boolean circuit representation based on modeling basic blocks. The program is then analyzed by a back-end SAT-based bounded model checker, where each unrolling is mapped to one step in a block-wise execution of the program. The main contributions of this paper are as follows: (1) Use of basic block-based unrollings with SAT-based bounded model checking of software programs. This allows us to take advantage of SAT-based learning inherent to the best performing bounded model checkers. (2) Various heuristics customized for models automatically generated from software, allowing a more efficient SAT-based analysis. (3) A prototype tool called F-SOFT has been implemented using our methodology. We present experimental results based on multiple case studies including a C-based implementation of a network protocol, and compare the performance gains using the proposed heuristics.