Formal Verification in a Commercial Setting

This tutorial addresses the following questions: ffl why do formal verification? ffl who is doing it today? ffl what are they doing? ffl how are they doing it? ffl what about the future? Introduction Formal methods long have been touted as a means to produce "provably correct implementations". It is only recently, however, with rather more modest claims, that one formal method: modelchecking, has been embraced by industry. In stark contrast with its two-decade development, only the last two years have laid witness to its commercial viability. Nonetheless, in this very short time, this technology has blossomed from scattered pilot projects at a very few commercial sites, into implementations in at least five commercially offered Design Automation tools. This acceleration of activity has even caught the attention of the investment community. Happy graduate students of this technology are basking in an unexpected competition for their talents in an otherwise lack-luster job market. W..