3 ms·
I recall my former professor at UT Austin, J Strother Moore, sharing how Intel utilized an Automatic Theorem Prover he helped create to spot bugs in processors.
by nopinsight 3y ago
I recall my former professor at UT Austin, J Strother Moore, sharing how Intel utilized an Automatic Theorem Prover he helped create to spot bugs in processors. But when engineers tweaked the design just a little, thinking it was a no-brainer that it wouldn't cause issues, they skipped the automated checks.
And just like that, the infamous Pentium bug hit the headlines globally.
- sn41 3y agoThanks for that nice anecdote. Moore is also famous for the Boyer-Moore string matching algorithm. Also, in the memory of Dr. Thomas R. Nicely (1943-2019), who found the bug: https://faculty.lynchburg.edu/~nicely/ https://faculty.lynchburg.edu/~nicely/