Formal verification technology has made significant advances in the last two decades. Techniques like model checking and theorem proving are now used in both the hardware and software industries. Current research is focused on increasing the scale and expressiveness of this technology. The biggest challenge facing this technology is in making it more accessible to a wider audience. This requires powerful automation, more integration, better user interfaces, and deeper embedding into design tools. To address these challenges, a two-day workshop on Usable Verification will be held at Microsoft Research in Redmond during November 15 and 16, 2010. This will be the first of a series of workshops aimed at building a community that is focused on usability issues in verification technology.
A workshop on Usable Verification was held during Nov 15-16, 2010, at Microsoft Research in Redmond, Washington. The workshop was attended by over fifty of the most distinguished researchers in the theory and practice of software and hardware verification. There was an honest appraisal of the stat e of practice of formal verification. Discussions at the workshop yielded several new creative ideas and research initiatives for improving the usability of verification technology and widening the base of applications. Suggestions covered empirical usability studies, crowd-sourcing, pricing models, zero-cost verification, system-level verification, better interfaces, and formal design tools. One noteworthy suggestion was to train graduate students in the use of verification technology. The workshop organizers acted on this suggestion to launch the Summer School on Formal Techniques. This school, funded out of the same project, was held at Menlo College during May 23-28, 2011. It was attended by over eighty graduate students, including several women and under-represented minority participants. The school featured lectures from distinguished researchers, invited talks, and hands-on laboratory sessions. Both the workshop and the school were regarded as highly successful by the participants. The workshop talks and material can be found at http://fm.csl.sri.com/UV10 and the lecture material associated with the summer school can be downloaded from http://fm.csl.sri.com/SSFT11.
