Approach to model construction:

Bandera's approach to model construction is to generate one model for each property to be checked. This approach is based on the observation that, given a specific property , many parts of the software may not influence at all. This allows Bandera to employ optimizations and abstractions that remove program components irrelevant to and thus generate a highly compacted model. Note that this customization approach generally is infeasible when one is generating models from programs by hand. One might naively complain that generating one model per property incurs significant overhead. However, it is often the case that checking a particular property without customizing the model is infeasible due to the exponential cost of model-checking. In addition, Bandera's philosophy is to design the customization so that cost of customization is always dominated by model-checking (i.e., in practice, the time to customize should be shorter than the time to model-check).