Efficient SAT-based bounded model checking for software verification |
| |
Authors: | Franjo Ivan?i? Zijiang Yang Malay K Ganai Aarti Gupta Pranav Ashar |
| |
Affiliation: | 1. NEC Laboratories America, 4 Independence Way, Ste. 200, Princeton, NJ 08540, United States;2. Department of Computer Science, Western Michigan University, 1903 W. Michigan Ave., Kalamazoo, MI 49008, United States |
| |
Abstract: | 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. |
| |
Keywords: | Software verification Bounded model checking SAT-based model checking |
本文献已被 ScienceDirect 等数据库收录! |
|