Using Software Model Checking for Software Component Certification

Recently, the notion of a third-party certifier has emerged. The certifier ensures that the published properties of a component have indeed been verified. While software certification can benefit component buyers and developers, we believe that the lack of techniques and standards has hampered the spread of its use. This research seeks to accomplish two goals: to develop state-space search strategies that enable us to use software model checkers to certify programs and to decrease the amount of intellectual property that the developer is required to share for certification.