The verified software repository: a step towards the verifying compiler |
| |
Authors: | JC Bicarregui CAR Hoare JCP Woodcock |
| |
Affiliation: | (1) Rutherford Appleton Laboratory, Chilton, Didcot, Oxon, OX11 0QX, UK;(2) Microsoft Research, Roger Needham Building, 7 J. J. Thomson Avenue, Cambridge, CB3 0FB, UK;(3) Department of Computer Science, University of York, Heslington, York, YO10 5DD, UK |
| |
Abstract: | The verified software repository is dedicated to a long-term vision of a future in which all computer systems justify the
trust that society increasingly places in them. This would be accompanied by a substantial reduction in the current high costs
of programming error, incurred during the design, development, testing, installation, maintenance, evolution, and retirement
of computer software. An important technical contribution to this vision will be a verifying compiler: a tool-set that automatically proves that a program will always meet its specification, insofar as this has been formalised,
without even needing to run it. This has been a challenge for computing research for over 30 years, but the current state
of the art now gives grounds for hope that it may be implemented in the foreseeable future. Achievement of the overall vision
will depend also on continued progress of research into dependability and software evolution, as envisaged by the UKCRC Grand
Challenge project in dependable systems evolution. The verified software repository is a first step towards the realisation of this long-term vision. It will maintain and
develop an evolving collection of state-of-the-art tools, together with a representative portfolio of real programs and specifications
on which to test, evaluate, and develop the tools. It will contribute initially to the inter-working of tools, and eventually
to their integration. It will promote transfer of the relevant technology to industrial tools and into software engineering
practice. It will build on the recognised achievements of practical formal development of safety-critical computer applications,
and contribute to an international initiative in verified software, covering theory, tools, and experimental validation.
Received April 2005
Revised November 2005
Accepted November 2005 by C. B. Jones |
| |
Keywords: | Grand challenges in computer science Dependable systems evolution Software engineering Verifying compiler Verified software repository Program verification Assertional reasoning Tools |
本文献已被 SpringerLink 等数据库收录! |
|