Refinement is the process of developing a more detailed design or implementation from an abstract specification through a sequence of mathematically-based steps that maintain correctness with respect to the original specification.

The aim of this BCS FACS refinement workshop is to bring together people who are interested in the development of more concrete designs or executable programs from abstract specifications using formal notations, tool support for formal software development, and practical experience with formal refinement methodologies.

The purpose of the workshop is to provide a forum for discussion of common ground and key differences. Questions we might centre discussions around include:

• What are the open problems in refinement?
• What scalable techniques are needed?

Topics of interest include (but are not limited to):

• Simulation techniques
• Foundations and semantics
• Case studies (specification and verification)
• Compositional and modular reasoning
• Object-orientation
• Time
• Specification notations
• Programming models
• Verification and tool support

Two types of contribution are elicited: tutorial or survey papers in addition to technical contributions.

• REFINE accepted papers
• REFINE program
• Participant list for REFINE

Proceedings

Informal proceedings will be available at the workshop. We aim to review and publish a selected number of the papers, after the conference, in a special issue of a leading journal.

History of the workshop

This workshop continues a long tradition in refinement workshops run under the auspices of the British Computer Society (BCS) FACS special interest group. Running since 1988, previous refinement workshops have been held at Cambridge, London, Bath etc.

In 1998 the BCS refinement workshop was combined with the Australasian Refinement Workshop to form the International Refinement Workshop, hosted at alongside Formal Methods Pacific 1998 at The Australian National University.

Workshop Webpage with more detailed information

http://www.cs.ukc.ac.uk/people/staff/eab2/refine/floc.html

Invited speakers

• Ralph-Johan Back and Joakim von Wright, Åbo Akademi U, Finland
  Compositional action system refinement
• Egon Börger, U Pisa, Italy
  Refinement method for Abstract State Machines
• Ana Cavalcanti, Federal U of Pernambuco, Brazil and Jim Woodcock, U Kent-Canterbury, UK
  Refinement of actions in Circus
• Jim Davies and Charles Crichton, Oxford U, UK
  Concurrency and refinement in the UML
• John Derrick and Eerke Boiten, U Kent-Canterbury, UK
  Unifying concurrent and relational refinement
• Kai Engelhardt, U New South Wales, Australia
  Towards a refinement theory that supports reasoning about knowledge and time for multiple agents
• David A. Naumann, Stevens Inst. of Techn., USA
  OO/higher order refinement calculus
• Emil Sekerinski, McMaster U, Canada
  Tabular verification and refinement
• Luke Wildman and C. J. Fidge, U Queensland, Australia
  The variety of variables in computer-aided real-time programming

Organizers

• John Derrick <J.Derrick@ukc.ac.uk>, U Kent-Canterbury, UK
• Eerke Boiten <eab2@ukc.ac.uk>, U Kent-Canterbury, UK
• Jim Woodcock <jcpw@ukc.ac.uk>, U Kent-Canterbury, UK
• Joakim von Wright <Jockum.Wright@abo.fi>, Åbo Akademi U, Finland