Harnessing Disruptive Innovation in Formal Verification

Technological innovations are sweeping through the field of formal verification. These changes are disruptive to tools based on interactive theorem proving, which needs new ways to integrate the capabilities of novel technologies. I describe two approaches. One is development and use of SMT solvers: these use techniques from theorem proving but apply them in ways that enable model checking, while also supporting highly automated theorem proving. The other is a proposal for an evidential tool bus: a loosely coupled architecture that allows many different verification components to collaborate to solve problems beyond the capability of any single component