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
.
(External)
BCS
The
(External)
British Computer Society
(BCS)
generously sponsored this event.
See
confirmed speakers/titles
below.
The
programme
and
(New)
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
BCS-FACS
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
(External)
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
(External)
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
(New)
Links from titles below are to
slides
where available or further
information otherwise.
See also
introduction
.
-
(External)
Dines Bjørner
,
DTU, Denmark
(External)
Domain Engineering
-
Michael Butler
,
University of Southampton, UK
Refinement of an Automatic Refinement Checker
-
(External)
Patrice Chalin
, Concordia University, Canada
Are Verifying Compiler Prototypes Matching User Expectations?
-
(External)
Rod Chapman
,
(External)
Praxis High Integrity Systems
, UK
Can we SPARK it? Well we'd like to, but...
-
(External)
David Crocker
,
(External)
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
-
(External)
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
-
(External)
Colin O'Halloran
,
(External)
QinetiQ
, UK
Ariane 5: Learning from Failure
-
(External)
Tony Hoare
,
(External)
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
(New)
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.
Maintained by
Prof. Jonathan Bowen
Last updated
12 August 2005