ePubs

The open archive for STFC research publications

Full Record Details

Persistent URL http://purl.org/net/epubs/work/12350513
Record Status Checked
Record Id 12350513
Title The Verified Software Repository: A step towards the Verifying Compiler
Contributors
Abstract The Verifed Software Repository is dedicated to a long-term vision of a future in which all computer systems justify the trust which Society increasingly places in them. This will 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 Program Verifer: a tool which automatically proves that a program will always meet its requirements, insofar as these have been formalised, without even needing to run it. This has been for over thirty years a challenge for computing research, but the current state of the art 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 Verifed 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 specfications on which to test, evaluate and develop the tools. It will contribute initially to the interworking of tools, and eventually to their integration. It will promote transfer of the relevant technology to industrial tools and into software engineering practice in UK. The Repository will build on the recognised achievements of UK in practical formal development of safety-critical computer applications, and it will establish UK as the leading nation in any future international initiative in Verfied Software, covering theory, tools and experimental validation.
Organisation CCLRC , ESC , VSR
Keywords Assertional reasoning , Grand challenges in computer science , Tools , Verified software repository , Dependable systems evolution , Program verification , Software engineering , Engineering , Verifying compiler
Funding Information
Related Research Object(s): 33971
Licence Information:
Language English (EN)
Type Details URI(s) Local file(s) Year
Preprint GC6 Steering Committee 2004. GC6-paper-20-12-2004.pdf 2004