Modular Checking of C Programs Using SAT-Based Bounded Model Checker

Static program analysis is promising as a complement to conventional testing methods relying on program executions. This paper introduces VARVEL, a SAT-based bounded model-checker for C programs. It has a notion of Design by Contract (DbC) explicitly and therefore modular checking of large C programs is achieved to resolve the scalability problem that model-checkers are usually faced with. Further, VARVEL provides advanced DbC features in that we can handle C programs having pointers to functions, re-entrancy problems, and defensive programming style. We also report some results of using VARVEL for the analysis of industrial C programs.