Software is at the core of the world’s infrastructure. We depend on it to control devices ranging from pacemakers to spacecraft, and to manage our banking, communication, and power distribution systems. Software failures can range from ones that are frequent and annoying, yet expensive to protect against, to those that are potentially life threatening and catastrophic. With the increasing ubiquity and complexity of software, its reliability represents a grand scientific challenge for computing.

Verification is a rigorous and systematic approach to asserting and demonstrating strong claims about the correctness of software. Verification is not just an abstract ideal. It is a practical tool for managing the complexity of the construction and use of software systems through the use of models, which act as simple yet accurate abstractions of software.

The technology of verification has been progressing rapidly in recent years and there are now a number of powerful and robust tools for building and analysing software. These tools are already being used to build and analyse models as well as to detect programming bugs. The primary challenge for verification technology is to establish its use in the systematic production of software that is accompanied by precisely specified claims, which are supported by rigorous justifications. The GC6 network is sponsored by EPSRC to explore the contribution of the UK to the international verified software initiative.

The Verified Software Initiative is an ambitious programme of research to develop the theory, technology, and infrastructure of software verification to a point where it is feasible to undertake the comprehensive verification of a wide variety of software systems with respect to a range of correctness properties. The current technology for verification has reached a stage at which a planned programme of collaborative endeavour could make a significant advance both to the basic science and to its beneficial application. The advance will be accompanied by a comprehensive programme of experiments that will continuously monitor the capabilities and limitations of the current state of the art in software verification, and will provide objective evidence when the tools are sufficiently mature to justify their incorporation into an industrial software design flow. By harnessing the idealism of the world’s best scientists on the central issues, the Verified Software Initiative will stimulate scientific breakthroughs that could well lead to rapid progress on the problems of specifying, designing, building, composing, certifying, and maintaining highly trustworthy software systems.

The industrial-scale software verification workshop aims to elicit problems in a range of UK software engineering domains to provide a focus for the future development of the Verified Software Initiative.

If you are interested in this initiative and wish to receive further details, please contact Tristram Armour.