The Verification Grand Challenge

Quite a bit of material relating to the Workshop on The Verification Grand Challenge, held February 21--23, 2005, at SRI International in Menlo Park, CA, is now available online. There are two sets of notes (taken by Sergey Berezin and Greg Morrisett) and the slides used by a majority of the speakers (including for keynotes by Tony Hoare and Amir Pnueli), as well as a few photos of the event.

I came away from the workshop more optimistic about the prospects for various program verification projects than I have been for several years. Impressive progress is being made by a number of researchers--some long-timers, some newcomers--using a variety of old and new approaches. (I try not to let the fact that I was similarly optimistic 30 years ago influence me too much.)

However, I also came away much less optimistic about a unified approach to the Verification Grand Challenge--at least on this side of the Atlantic. This is partly because none of the usual sources of IT research funding is currently prepared to make major investments in projects with a 10-15 year timescale. However, it is more because the sheer variety of the approaches being taken by the best investigators (who should provide the core of a Grand Challenge team) makes it unlikely that a sufficient number of them will subordinate their own research interests to those of an overarching project.

There still seems to be some likelihood of the European Union pulling together a Verification Grand Challenge team. A lot of the top researchers are there, and the EU has a track record of putting more of its IT research investments into collaborative projects. So much the better for them. If they succeed, we will all benefit.