The major extant hurdle to a more widespread use of formal methods like model checking in systems design is the limited capacity of the algorithms. While most key problems in formal verification are theoretically intractable, the last decade has witnessed algorithmic improvements that have greatly extended the realm of what can be done both rigorously and automatically. Continued increase in capabilities is a priority for most large electronic design organizations.
Recent advances in formal verification technology have been particularly remarkable in abstraction refinement and in the procedures based on propositional satisfiability. These advances have been made possible by clever uses of decision procedures and even by the cooperation of different approaches. However, little has been done in leveraging the strengths of different approaches via a deeper integration. Current techniques often fail on problems that require a combination of strengths from different approaches, rather than the choice of a suitable approach from a toolbox. The aim of this proposal is to pursue such integration and to explore the benefits that come from realizing that the separation of abstraction-based model checking and decision procedures is an artificial one. The anticipated result is an effective strategy for large scale model checking that represents a significant leap in capacity.
The strength and, at the same time, weakness of satisfiability (SAT) solvers is their ability to forget. While fixpoint computations accumulate sets of states whose representations often become unwieldy, a SAT solver can, in principle, avoid saving any information about the search except for the decision stack. The price of forgetfulness is repetition, and even though modern SAT procedures record conflict clauses, one encounters problems where such procedures flounder because of their inability to represent the relevant information about subproblems already solved. The proposed research will address this issue in the context of abstraction-based model checking. A significant fallout for other applications of satisfiability and for the general problem of combinatorial search is also expected.
