COMPLETE SAT-BASED MODEL CHECKING FOR CONTEXT-FREE PROCESSES

A complete SAT-based model checking algorithm for context-free processes is presented. We reduce proof search in local model checking to Boolean satisfiability. Bounded proof search can therefore be performed by SAT solvers. Moreover, the completeness of proof search is reduced to Boolean unsatisfiability and hence can be checked by SAT solvers. By encoding the local model checking algorithm in [13], SAT solvers are able to verify properties in the universal fragment of alternation-free mu-calculus formulae on context-free processes. Since software programs can be modeled by context-free processes, our result demonstrates that a purely SAT-based algorithm for software verification is indeed possible.