1.2. Bogor Overview

To meet the challenges of using model checking in the context of current trends in software development outlined in previous section, we have constructed an extensible and highly modular explicit-state model checking framework called Bogor . Using Bogor, we seek to enable more effective incorporation of domain knowledge into verification models and associated model checking algorithms and optimizations, by focusing on the following principles.

In summary, we believe that a number of trends in software development suggest the need for flexible and adaptable infrastructure to enable practitioners to more effectively develop model checking tools that are customized to particular domains and development processes. While there are many avenues that one might pursue, we believe that the Bogor framework provides a robust and well-reasoned foundation that researchers and practitioners can use to address important facets of automated reasoning for modern software systems.