Refinement Workshop
Copenhagen, Denmark, July 20-21, 2002
Affiliated with FME 2002

Refinement is one of the cornerstones of a formal approach to software engineering.

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.


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

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