3. ICFEM 2000: York, England, UK

Invited Speaker

• David Lorge Parnas:
  The Use of Mathematics in Software Engineering. 1
  

Development

• Toomas P. Plaks:
  Formal Derivation of Multilayered Hardware/Software Structures. 5-14
  
• Antoine Requet, Gaëlle Bossu:
  Embedding Formally Proved Code in a Smart Card: Converting B to C. 15-
  

Structuring

• Kevin Lano, Kelly Androutsopoulos, Pauline Kan:
  Structuring Reactive Systems in B AMN. 25-34
  
• Michihiro Matsumoto, Kokichi Futatsugi:
  Highly Reliable Component-Based Software Development by Using Algebraic Behavioral Specification. 35-44
  
• Arun Venkataraman, Murali Rangarajan, Perry Alexander:
  Composing Specifications in VSPEC. 45-
  

Algebraic Approaches

• Mohamed Jmaiel:
  A Unified Algebraic Framework for Specifying Communication Protocols. 57-66
  
• Tetsuo Tamai:
  Formal Treatment of a Family of Fixed-Point Problems on Graphs by CafeOBJ. 67-
  

Invited Speaker

• C. A. R. Hoare:
  Legacy Code. 75
  

Verification

• Hong Peng, Sofiène Tahar, Ferhat Khendek:
  SPIN vs. VIS: A Case Study on the Formal Verification of the ATMR Protocol. 79-88
  
• Dmitri Chkliaev, Jozef Hooman, Peter van der Stok:
  Mechanical Verification of Transaction Processing Systems. 89-
  

Formal and Informal Notations

• Claudia Pons, Gabriel Baum:
  Formal Foundations of Object-Oriented Modeling Notations. 101-110
  
• Wolfgang Grieskamp, Markus Lepper:
  Using Use Cases in Executable Z. 111-120
  
• Ian MacColl, David A. Carrington:
  Translating UAN into CSP. 121-
  

Retrenchment

• Richard Banach:
  Maximally Abstract Retrenchments. 133-142
  
• Richard Banach, Michael Poppleton:
  Fragmented Retrenchment, Concurrency and Fairness. 143-
  

Invited Speaker

• Werner Damm:
  Offering Formal Verification Capabilities for Industry Standard Case Tools: Challenges and Results. 153
  

Z: Theory and Practice

• Ali E. Abdallah:
  Filter Promotion Transformation Strategies for Deriving Efficient Programs from Z Specifications. 157-168
  
• R. D. Arthan, P. Caseley, Colin O'Halloran, Alf Smith:
  ClawZ: Control Laws in Z. 169-176
  
• Chris J. Taylor, John Derrick, Eerke A. Boiten:
  A Case Study in Partial Specification: Consistency and Refinement for Object-Z. 177-
  

Animation

• Ali E. Abdallah, Mark Green:
  An Integrated CSP-Based Tool for the Visualisation, Animation and Performance Evaluation of Message Passing Algorithms. 189-
  
• Jonathan P. Bowen, Jifeng He, Qiwen Xu:
  An Animatable Operational Semantics of the Verilog Hardware Description Language. 199-208