Grand Challenge 6
Workshop on Dependable Systems Evolution
18 July 2005, University of Newcastle upon Tyne↑, UK
The British Computer Society (BCS) generously sponsored this event.
See speakers/titles below. The programme and full proceedings (2Mbytes) are also available. This was Workshop 3 on the Registration Form of the FM05 conference and was located in Beehive 221. Please note that you may register independently of the main conference if you wish.
| Jonathan Bowen|
Institute for Computing Research
London South Bank University
Faculty of BCIM, Borough Road
London SE1 0AA
tel: 020 7815 7462
fax: 020 7815 7793
| Jim Woodcock|
Department of Computer Science
University of York
York YO10 5DD
email: jim AT cs.york.ac.uk
tel: 01904 434335
fax: 01227 726811
The UK Computing Research Committee has been discussing how best to advance computing research; they held a workshop in Edinburgh↑ in November 2002, which produced seven proposals for grand challenges in computer science. This workshop was part of a series that brings together international researchers to discuss the sixth challenge on Dependable Systems Evolution, which was inspired by the challenge of the Verifying Compiler.
The long-term aim of the project is to produce a coherent software engineering tool-set based on formal principles, to aid in the development, deployment, and evolution of dependable systems; and to submit the tools to convincing large-scale evaluation on a heterogeneous range of challenge codes. The aim of this particular workshop was to produce an authoritative account of the current state of the art in strong software engineering tool-sets, and their application to systems that have been deployed in practice.
Topics of interest include the following areas:
- Tools: descriptions of existing tools; capabilities and limitations; comparisons with other tools; plans for extensions; integration of tools.
- Applications: experiences of strong software engineering; scalability; application domains, including all areas of dependability and evolution.
- Position papers: theoretical issues, levels of assurance, suitable exemplars, future technologies, annotated bibliographies, technical problems and obstacles.
We may base a survey article on the accepted papers and workshop discussion.
Speakers and titlesEdit
- Dines Bjørner, DTU, Denmark
- Michael Butler, University of Southampton, UK
Refinement of an Automatic Refinement Checker
- Patrice Chalin, Concordia University, Canada
Are Verifying Compiler Prototypes Matching User Expectations?
- Rod Chapman, Praxis High Integrity Systems, UK
Can we SPARK it? Well we'd like to, but...
- David Crocker, Escher Technologies, UK
Verifying Compilers for Financial Applications
- Massimo Felici, University of Edinburgh, UK
Modelling Safety Case Evolution: Examples from the Air Traffic Management Domain
- Joseph Kiniry, University College Dublin, Ireland
Supporting Multiple Theories and Provers in ESC/Java2
- Cliff Jones, University of Newcastle upon Tyne, UK
Technical Challenges for Verification in Design
- Colin O'Halloran, QinetiQ, UK
Ariane 5: Learning from Failure
- Tony Hoare, Microsoft Research, Cambridge, UK
The Ideal of Verified Software
- Lawrence Paulson, University of Cambridge, UK
Integrating Interactive and Automatic Theorem Provers: Status and Prospects
- Peter Sewell, University of Cambridge, UK
Specification and Testing using a General-purpose Proof Assistant: TCP, UDP and Sockets in HOL
The programme and proceedings (2Mbytes) are available. Information about a new UK EPSRC↑ VSR-net (Verified Software Repository) Network was also be given at the Workshop, starting in September 2005 for three years.
Maintained by Prof. Jonathan Bowen
Last updated 11 April 2009