ZB 2003: Turku, Finland

• Daniel Jackson:
  Alloy: A Logical Modelling Language. 1
  Electronic Edition (Springer LINK) BibTeX
• Susan Stepney, Fiona Polack, Ian Toyn:
  An Outline Pattern Language for Z: Five Illustrations and Two Tables. 2-19
  Electronic Edition (Springer LINK) BibTeX
• Susan Stepney, Fiona Polack, Ian Toyn:
  Patterns to Guide Practical Refactoring: Examples Targetting Promotion in Z. 20-39
  Electronic Edition (Springer LINK) BibTeX
• Sandrine Blazy, Frédéric Gervais, Régine Laleau:
  Reuse of Specification Patterns with the B Method. 40-57
  Electronic Edition (Springer LINK) BibTeX
• Helen Treharne, Steve Schneider, Marchia Bramble:
  Composing Specifications Using Communication. 58-78
  Electronic Edition (Springer LINK) BibTeX
• Frédéric Peschanski, David Julien:
  When Concurrent Control Meets Functional Requirements, or Z + Petri-Nets. 79-97
  Electronic Edition (Springer LINK) BibTeX
• Guilhem Pouzancre:
  How to Diagnose a Modern Car with a Formal B Model?. 98-100
  Electronic Edition (Springer LINK) BibTeX
• Stefan Hallerstede:
  Parallel Hardware Design in B. 101-102
  Electronic Edition (Springer LINK) BibTeX
• Moshe Deutsch, Martin C. Henson, Steve Reeves:
  Operation Refinement and Monotonicity in the Schema Calculus. 103-126
  Electronic Edition (Springer LINK) BibTeX
• John Derrick, Heike Wehrheim:
  Using Coupled Simulations in Non-atomic Refinement. 127-147
  Electronic Edition (Springer LINK) BibTeX
• Moshe Deutsch, Martin C. Henson:
  An Analysis of Forward Simulation Data Refinement. 148-167
  Electronic Edition (Springer LINK) BibTeX
• Jean-Raymond Abrial:
  B^#: Toward a Synthesis between Z and B. 168-177
  Electronic Edition (Springer LINK) BibTeX
• Steve Dunne:
  Introducing Backward Refinement into B. 178-196
  Electronic Edition (Springer LINK) BibTeX
• Bill Stoddart, Frank Zeyda:
  Expression Transformers in B-GSL. 197-215
  Electronic Edition (Springer LINK) BibTeX
• Annabelle McIver, Carroll Morgan, Thai Son Hoang:
  Probabilistic Termination in B. 216-239
  Electronic Edition (Springer LINK) BibTeX
• Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, Carroll Morgan:
  Probabilistic Invariants for Probabilistic Machines. 240-259
  Electronic Edition (Springer LINK) BibTeX
• Graeme Smith, Kirsten Winter:
  Proving Temporal Properties of Z Specifications Using Abstraction. 260-279
  Electronic Edition (Springer LINK) BibTeX
• Kirsten Winter, Graeme Smith:
  Compositional Verification for Object-Z. 280-299
  Electronic Edition (Springer LINK) BibTeX
• John Derrick:
  Timed CSP and Object-Z. 300-318
  Electronic Edition (Springer LINK) BibTeX
• Mark Utting, Shaochun Wang:
  Object Orientation without Extending Z. 319-338
  Electronic Edition (Springer LINK) BibTeX
• Nuno Amálio, Fiona Polack:
  Comparison of Formalisation Approaches of UML Class Constructs in Z and Object-Z. 339-358
  Electronic Edition (Springer LINK) BibTeX
• Bertrand Meyer:
  Towards Practical Proofs of Class Correctness. 359-387
  Electronic Edition (Springer LINK) BibTeX
• Robert M. Hierons, Mark Harman, Harbhajan Singh:
  Automatically Generating Information from a Z Specification to Support the Classification Tree Method. 388-407
  Electronic Edition (Springer LINK) BibTeX
• Christophe Darlot, Jacques Julliand, Olga Kouchnarenko:
  Refinement Preserves PLTL Properties. 408-420
  Electronic Edition (Springer LINK) BibTeX
• Marc Frappier, Régine Laleau:
  Proving Event Ordering Properties for Information Systems. 421-436
  Electronic Edition (Springer LINK) BibTeX
• Mark Utting, Ian Toyn, Jing Sun, Andrew Martin, Jin Song Dong, Nicholas Daley, David W. Currie:
  ZML: XML Support for Standard Z. 437-456
  Electronic Edition (Springer LINK) BibTeX
• Jean-Raymond Abrial, Dominique Cansell, Dominique Méry:
  Formal Derivation of Spanning Trees Algorithms. 457-476
  Electronic Edition (Springer LINK) BibTeX
• Carla Ferreira, Michael J. Butler:
  Using B Refinement to Analyse Compensating Business Processes. 477-496
  Electronic Edition (Springer LINK) BibTeX
• Christine Poerschke, David E. Lightfoot, John L. Nealon:
  A Formal Specification in B of a Medical Decision Support System. 497-512
  Electronic Edition (Springer LINK) BibTeX
• Lilian Burdy, Antoine Requet:
  Extending B with Control Flow Breaks. 513-527
  Electronic Edition (Springer LINK) BibTeX
• Nazareno Aguirre, Juan Bicarregui, Theodosis Dimitrakos, T. S. E. Maibaum:
  Towards Dynamic Population Management of Abstract Machines in the B Method. 528-545
  Electronic Edition (Springer LINK) BibTeX