The Grand Challenge in Verified Software - Introduction

1. Context

2. Another way?

3. A grand challenge

4. Deliverables

5. Meetings

6. Research roadmap

7. Goals of the Repository

Context

Industrial software usually has extensive documentation, but software behaviour often comes as a complete surprise!  Programming is inherently hard because we have to reduce a problem to a set of rules that can be blindly followed by a computer.  But components interact and interfere, and undesirable properties emerge. The result is that systems fail to satisfy their users’ needs.

Software is inherently hard to develop.  It’s hard to define requirements, to anticipate interactions, and to accommodate new functionality.  Documentation involves large amounts of text, pictures, and diagrams, but these are often imprecise and ambiguous.  Important information is often hidden by irrelevant detail.  Design mistakes are often discovered too late, making them expensive or even impossible to correct.  It’s a tribute to the skill of software engineers that systems work at all.

Another way?

Some practitioners in industry and researchers from universities believe it’s now practical to use formal methods to produce software, even non-critical software.  And that this will turn out to be the cheapest way to do it.  Given the right computer-based tools, the use of formal methods could become widespread and transform the industrial practice of software engineering.  The computer science community recently committed itself to making this a reality within the next fifteen to twenty years.

A grand challenge

In 2004, Tony Hoare proposed automatically verified software as a grand scientific challenge for computing. 

If the grand challenge project is successful, then in fifteen years' time we'll have convincing evidence to change standard industrial practice.

Deliverables

1. A comprehensive theory of programming covering the features needed to build practical and reliable programs.

2. A coherent toolset automating the theory and scaling up to large codes.

3. A collection of verified programs replacing existing unverified ones, continuing to evolve as verified code: the Verified Software Repository (VSR).

Meetings

In the last three years a research agenda has started to emerge through a series of meetings and publications.

• NSF-funded meetings in the US.  (February 2005)

• EPSRC-funded meetings in the UK. 

  • Workshop on Dependable Systems Evolution, 13-14 November 2003, Queen Mary, University of London.

  • Workshop on Dependable Systems Evolution, 18 March 2004, Gresham College, London.

  • Workshop on the Verified Software Repository, 21 December 2004, BSC-FACS Christmas Meeting, London.

  • Grand Challenge Workshop on Dependable Systems Evolution (GCW-DSE), 2-3 April 2005, (a Satellite Workshop of ETAPS 2005) Edinburgh.

• The VSTTE conference -- Verified Software: Theories, Tools, & Experiments -- was held at ETH Zürich during 10-13 October 2005, as a working conference of IFIP (the International Federation for Information Processing), specifically TC2 (the IFIP committee on programming) and its Working Group 2.3 (Programming Methodology).

• Cliff B. Jones, Peter W. O'Hearn, Jim Woodcock: Verified Software: A Grand Challenge.  IEEE Computer 39(4): 93-95 (2006).

• Jim Woodcock: First Steps in the Verified Software Grand Challenge.  IEEE Computer 39(10): 57-64 (2006).

• Juan Bicarregui, C. A. R. Hoare, J. C. P. Woodcock: The verified software repository: a step towards the verifying compiler. Formal Aspects of Computing 18(2): 143-151 (2006).

Research roadmap

The developing research roadmap is available at the QPQ website. A useful roadmap should set out long-term co-ordinated programme of incremental research.

1. Accelerated scaling of the performance, robustness, and functionality of basic verification technology.

2. Integration and embedding of this technology in program development and verification methodologies and environments, and in teaching.

3. Pilot projects to evaluate feasibility and guide technology development.

4. Large-scale experiments that benchmark the technology.

Goals of the Repository

1. To accelerate the development of verification technology through the development of better tools, greater interoperability, and realistic benchmarks.

2. To provide a focus for the verification community to ensure that the research results are relevant, replicable, complementary, and cumulative, and promote  meaningful collaboration between complementary techniques.

3. To provide open access to the latest results and educational material in areas relevant to verification research.

4. To collect a significant body of verified code (specification, derivation, proofs, implementation) that addresses challenging applications.

5. Identify key metrics for evaluating the scale, efficiency, depth, amortization, and reusability of the technology.

6. Enumerate challenge problems and areas for verification, preferably ones that require multiple techniques.

7. Identifying (and eventually standardising) formats for representing and exchanging specifications, programs, test cases, proofs, and benchmarks, to support tool interoperability and comparison.

8. Defining quality standards for the contents of the repository.

Page created by Jim Woodcock, 18th June 2007, last updated by Juan Bicarregui, 6th August 2007