One of the major challenges is how to abstract the program to a high-level description.

Conventional model checkers assume that the design is described at a high level that abstracts away many details of the actual implementation. A great deal of manual effort is required to build "models" before testing programs. Moreover, in the abstraction process, possible human errors would result in missing bugs and causing false alarms during verification, further increasing the cost and reducing the usefulness of model checking. When a program is large and complex, the abstraction process becomes more difficult. To address this challenge, the two assigned papers proposed two different methods.

In the first paper, Musuvathi et al. developed an implementation-level model checker, CMC, which checks C and C++ implementations directly. That is, CMC eliminates the need for a separate abstract description of the system's behavior. This method reduces the effort to use model checking, and reduces missed errors as well as time-wasting false error reports resulting from inconsistencies between the abstract description and the actual implementation. Additionally, changes in the implementation can be checked immediately without updating a high-level description.

Despite the advantages mentioned above, the implementation-level model checker introduces a much larger state space. Conventional model checking techniques have to handle the problem of state space explosion even for moderately sized systems. As CMC deals directly with implementations rather than their abstract models, CMC confronts much larger state spaces than conventional model checkers. Even though several approaches were proposed to reduce the states efficiently, such as incremental heap canonicalization and exploring only interesting protocol behaviors, this limitation could be a great encumbrance when the abstraction-free model checker is applied to more complex programs.

In the second paper, Ball et al. addressed this problem by automatically abstracting the C code of a device driver to a Boolean program, which has all the control-flow constructs of C (including procedures and procedure calls) but only Boolean variables. These variables track the state of relevant Boolean expressions in the C program. Such abstraction can preserve all code errors: any violation that appears in the original code also appears in the abstraction. Moreover, this abstraction method can automatically separate the relevant state from the irrelevant state so that the amount of state that needs to be tracked is small compared to the entire program state.

The limitation of boolean programs is that they may add too many spurious paths (false errors) and hurt the effectiveness of model checkers. In order to enable sound verification of reachability properties, boolean programs are constructed by over- approximating the behavior of the original program; this results in adding false errors. Therefore, model checking techniques based on boolean programs must refine the abstraction (through the addition of new predicates) to eliminate false errors. This is time consuming.