Nov
Dynamic vs Formal papers – lets be fair!
I have just returned from the Haifa Verification Conference in Israel, and I have to say – what a wonderful little conference. This was originally an internal event for the IBM research labs in Haifa to share their experiences and research with each other, but opened it up to all verification experts some years ago. IBM still does all of the organization, provides the facilities, and makes it as easy as possible for everyone else to contribute and learn as a community. The program committee has an impressive line-up of experts in the field to ensure that there is a good balance in the papers that are presented.
Some of the presentations were very high level, such as the one given by Daniel Jackson of MIT and one given by Yoav Hollander, who paves the way for Cadence in verification. The presentation by Moshe Vardi of Rice University was a great introduction to some of the past and current work in the area of formal methods. Others were very technical; especially those dealing with formal methods research, but the presenters were great in treating people like me, who have grown up with dynamic verification methods, with a lot of patience.
Wednesday concentrated on dynamic simulation methods, and was by far the most well attended day. Most of the extras were IBM folks. It occurred to me that while these sessions were the best attended, it is rare to see many papers on dynamic methods in conferences such as DAC. I asked a few people and got the general response: well that’s because there hasn’t been anything new there worth writing papers about. I accepted this for a while, but then got to thinking and after listening to a few other papers on formal methods I got to thinking: hang on a minute. They just published a paper because they were 10% faster that a previous algorithm. We do that in the dynamic simulation world all the time and nobody thinks it is worth reporting. Do we have very different standards here? Just because dynamic methods are, well, sloppy in comparison, we are improving algorithms and user productivity all the time at substantially higher levels than many of these papers are reporting. Maybe that is a better way to judge advancements: not by how long it takes to run, but how much does it improve productivity for an end user. If that were the case, then I think we would see conferences dominated by dynamic verification methods.
A quick thanks to everyone who made HVC08 possible, including Certess and Synopsys who partially sponsored my attendance there as an invited speaker.
