Refinement Workshop 2005 Program

12 April 2005, co-located with ZB 2005
REFINE 2005 - BCS FACS - EPSRC RefineNet


Registration for the workshop is being dealt with via the ZB conference website.


The workshop proceedings will appear in Electronic Notes in Theoretical Computer Science. BCS-FACS will provide a best paper prize. The journal Formal Aspects of Computing will publish a special issue, consisting of developments and extensions of the best workshop papers.


10 - 11.30am - Automation

Using the Alloy analyser to verify data refinement in Z
C Bolton

Model checking downward simulations
G Smith and J Derrick

Simpler reasoning about system properties - a proof by refinement technique
D Atiya and S King and J Woodcock

11:30 - 12 - Morning tea

12 - 13:30 - Theory I

Angelic non-determinism and unifying theories of programming
A Cavalcanti and J Woodcock

nuZ - a wide spectrum logic
M Henson and B Kajtazi

An analysis of operation refinement in an abortive paradigm
M Deutsch

13:30 - 14:30 - Lunch

14:30 - 16:00 - Theory II

Verifying concurrent data structures by simulation
R Colvin, S Doherty, L Groves and M Moir

Tank monitoring: a pAMN case study
S Schneider, T Hoang, K Robinson and H Treharne

Breaking the model: finalisations and a taxonomy of security attacks
J Clark and S Stepney and H Chivers

16:00 - 16:30 - Afternoon tea

16:30 - 18:00 - OO and applications

Refinement patterns for UML
K Lano and K Androutsopolous and D Clark

Refinement via consistency checking in MDA
R Paige  and D Kolovos and F Polack

Emergent properties do not refine
F Polack and S Stepney