A one-day
Workshop on Monday 18 July 2005 at the
FM05 Formal Methods Conference, Newcastle upon Tyne, UK,
The
British Computer Society (BCS)
generously sponsored this event.
|
See
confirmed 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@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
Website: www.fmnet.info/gc6/fm05
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 EPSRC
VSR-net (Verified Software Repository)
Network was also be given at the Workshop, starting in September 2005
for three years.