My favorite tale about testing is from AMD effort. They hired ACL experts to verify their FPU. These experts have built a translator from Verilog to ACL and then formally verified resulting ACL code. They found several bugs that slipped 84 million test suite.
This was done by Boyer and Moore (the same names behind the Boyer–Moore string search algorithm) at Computational Logic, Inc. The automated reasoning software that thesz is referring to here is ACL2, and not that other Austin export that goes by the name ACL.
While you might be referring to Austin City Limits (the television show), you might also be referring to the ACL Festival, which didn't launch until 2002.
