Formal Verification of Real-World Hardware -
Testing remains the primary strategy for software and hardware designs today, but how can we be sure that our designs are correct when we have only tested a small subset of their potential inputs? Formal verification provides an alternative to testing where we prove the design is correct for all inputs. As our tools improve and the consequences of bugs increase, formal verification is becoming ever more compelling. In this talk, we will discuss the state of formal verification in industry and the challenges we currently have to applying it to industrial hardware designs. These challenges include tool capacity limitations, inadequate specifications, complex input modeling, and dealing with constant change. We will further discuss how these challenges are being overcome in critical domains, enabling formal verification to be applied to a growing set of real computing products we all use every day.

Bio: Erik is currently working at Apple, apllying formal verification to hardware designs. Prior to Apple, Erik worked for 14 years at Intel and was part of the team that formally verified the execution cluster of the first generation Core i7. He recieved a B.S. in Electrical Engineering and Computer Science from the University of California at Berkeley and a M.S. and Ph.D. in Computer Science from the University of Texas at Austin. His thesis involved the sound combination of fully automated SAT-solver-based strategies into a higher-level logic and automated theorem prover.  Outside of work, Erik is raising three girls and enjoys hiking and running in our wonderful Oregon outdoors.