>Certainly, and I didn't claim that there was no more left to do. I merely
>pointed out that 6 year old work wasn't the state of the art.
Cohn's paper is not an uptodate survey of current work, but that's not why
I mentioned it.
>I do think that there are problems that can be solved now. Miriam Leeser
>(of Cornell) has been doing work on verifying hardware much like the FP
>hardware that caused the bug in the Pentium. I don't think that finding
>such bugs is beyond the state of the art.
It's my impression that applying theorem proving
to any but the most trivial hardware now requires an immense effort and
that there are important limitations on what can be modeled. The
relative success of model checking methods and the incorporation
of simulation and model checking into many of the "theorem proving"
efforts indicates, to me, that the state of the art is still quite limited.
That's not to say that no progress is being made and I'd be happy to
find out that my impression is based on nothing more than outdated
literature. In much of computer science, however,
there is a tendency to overestimate progress, and the hardware verification
community has not been an exception.