Formal Verification - History

Theory has been around for a long time
- Size of systems to be verified: 10^6
A major breakthrough in 1990 (Clarke et al., CMU)
- Size of systems to be verified: 10^20
Subtle bugs were found in real systems by formal verification
- Cache coherency protocol, Encore Gigamax (McMillan)