2011 Refinement Workshop at FM '11

20 June 2011, colocated with FM 2011 at Limerick

Room KBG-13, Kemmy Business School.

Programme

• 9:55 opening
• 10:00 Maria Teresa Llano Rodriguez, Andrew Ireland and Alison Pease. Discovery of Invariants through Theory Formation
• 10:30 coffee
• 11:00 Gian Perrone, Soren Debois and Thomas Hildebrandt. Bigraphical Refinement
• 11:30 John Derrick, Anthony Simons and S North. Building a refinement checker for Z
• 12:00 short break
• 12:10 Cesar Rodrigues, Manuel A. Martins, Alexandre Madeira and Luis Barbosa. Refinement by interpretation in Pi-institutions
• 12:40 Alvaro Miyazawa and Ana Cavalcanti. Refinement-based verification of sequential implementations of Stateflow charts
• 13:00 lunch
• 14:10 Steve Reeves and David Streader. Refinement for Probabilistic Systems with Nondeterminism
• 14:40 Ukachukwu Ndukwu and Annabelle Mciver. Model exploration and analysis for quantitative safety in probabilistic B
• 15:10 Richard Banach, Huibiao Zhu, Wen Su and Runlei Huang. Formalising the Continuous/Discrete Modeling Step
• 15:30 tea
• 16:00 Steve Schneider, Helen Treharne and Heike Wehrheim. A CSP Account of Event-B Refinement
• 16:30 Eerke Boiten. Perspicuity and granularity in refinement
• 17:00 Pontus Bostrom, Fredrik Degerlund, Kaisa Sere and Marina Walden. Concurrent Scheduling of Event-B Models
• 17:30 end

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 the exchange of ideas, and discussion of common ground and key differences.

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

Proceedings

Workshop proceedings have been published in Electronic Proceedings in Theoretical Computer Science. A special issue of Formal Aspects of Computing will be produced afterwards, consisting of developments and extensions of workshop papers. These will be refereed in the usual fashion prior to acceptance by the journal.

Program committee

• Eerke Boiten, University of Kent, UK (co-chair)
• John Derrick, University of Sheffield, UK (co-chair)
• Steve Reeves, University of Waikato, NZ (co-chair)
• Richard Banach, University of Manchester, UK
• Luis Barbosa, University of Minho, PT
• Andrew Butterfield, Trinity College Dublin and LERO, Ireland
• Ana Cavalcanti, University of York, UK
• Yifeng Chen, Peking University, PR China
• Steve Dunne, Teesside University, UK
• Lindsay Groves, Victoria University of Wellington, NZ
• Stefan Hallerstede, Heinrich-Heine-Universitaet Duesseldorf, Germany
• Eric Hehner, University of Toronto, Canada
• Wim Hesselink University of Groningen, NL
• Stephan Merz, Inria Nancy and LORIA, France
• Marcel Oliveira, Universidade Federal do Rio Grande do Norte, Brazil
• Gerhard Schellhorn, Augsburg University, Germany
• Steve Schneider, University of Surrey, UK
• Emil Sekerinski, McMaster University, Canada
• Graeme Smith, University of Queensland, Australia
• Helen Treharne, University of Surrey, UK
• Heike Wehrheim, University of Paderborn, Germany