Programs as Models Program model checkers simply model check programs directly. They often adopt a modeling notation which is—or is close to—some popular implementation language such as C or Java (Visser et al. 2003; Stoller 2000; Musuvathi et al. 2002). The best possible scenario is when the language of the target program and the modeling notation are exactly the same. In this case, the program can be model checked almost directly without the need for constructing a separate model—the program itself is used as the model. This can reduce the cost of analysis by reducing the effort required to construct and maintain separate and explicit models. It also avoids the maintenance cost of trying to keep the models and the code consistent as the software is modified.
In general, however, it’s not possible to avoid the construction of a separate model because of factors such as the mismatch between the modeling and target notations or the required level of detail in the model. It is often necessary to apply a combination of the techniques mentioned above to obtain a valid representation of the program to be analyzed. Parts of the system may be modeled manually, whereas other parts may lend themselves to direct translation.