Grand Challenge 6
Workshop on Dependable Systems Evolution
18 July 2005, University of Newcastle upon Tyne↑, UK
A one-day Workshop on Monday 18 July 2005 at the FM05 Formal Methods Conference, Newcastle upon Tyne, UK, 18–22 July 2005, organized by the GC6 Committee.
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.
Main organizers/chairs[]
| Jonathan Bowen Institute for Computing Research London South Bank University Faculty of BCIM, Borough Road London SE1 0AA email: jonathan.bowen@lsbu.ac.uk tel: 020 7815 7462 fax: 020 7815 7793 |
Jim Woodcock Department of Computer Science University of York Heslington York YO10 5DD email: jim AT cs.york.ac.uk tel: 01904 434335 fax: 01227 726811 |
Paul Boca (Secretary of the BCS Formal Aspects of Computing Science Specialist Group) helped with the organization of the Workshop and his attendance was supported by BCS-FACS.
General information[]
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 titles[]
Links from titles below are to slides where available or further information otherwise. See also introduction.
- Dines Bjørner, DTU, Denmark
Domain Engineering - 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