FME 2002: Copenhagen, Denmark

• Natarajan Shankar:
  Little Engines of Proof. 1-20
  
• Bruno Legeard, Fabien Peureux, Mark Utting:
  Automated Boundary Testing from Z and B. 21-40
  
• Gil Ratsaby, Baruch Sterin, Shmuel Ur:
  Improvements in Coverability Analysis. 41-56
  
• Juan C. Burguillo-Rial, Manuel J. Fernández Iglesias, Francisco J. González-Castaño, Martín Llamas Nistal:
  Heuristic-Driven Test Case Selection from Formal Specifications. A Case Study. 57-76
  
• Igor B. Bourdonov, Alexander Kossatchev, Victor V. Kuliamin, Alexander K. Petrenko:
  UniTesK Test Suite Architecture. 77-88
  
• David von Oheimb, Tobias Nipkow:
  Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited. 89-105
  
• Juan Bicarregui:
  Do Not Read This. 106-125
  
• Niels Jørgensen:
  Safeness of Make-Based Incremental Recompilation. 126-145
  
• Sharon Barner, Shoham Ben-David, Anna Gringauze, Baruch Sterin, Yaron Wolfsthal:
  An Algorithmic Approach to Design Exploration. 146-162
  
• Alexandre Mota, Paulo Borba, Augusto Sampaio:
  Mechanical Abstraction of CSP_Z Processes. 163-183
  
• Thomas Arts, Clara Benac Earle, John Derrick:
  Verifying Erlang Code: A Resource Locker Case-Study. 184-203
  
• Michael Huber, Steve King:
  Towards an Integrated Model Checker for Railway Signalling Data. 204-223
  
• Anthony Hall:
  Correctness by Construction: Integrating Formality into a Commercial Development Process. 224-233
  
• Darko Marinov, Sarfraz Khurshid:
  VAlloy - Virtual Functions Meet a Relational Language. 234-251
  
• Vlad Rusu:
  Verification Using Test Generation Techniques. 252-271
  
• Néstor Cataño, Marieke Huisman:
  Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java. 272-289
  
• Ludovic Casset:
  Development of an Embedded Verifier for Java Card Byte Code Using Formal Methods. 290-309
  
• Michael Backes, Christian Jacobi, Birgit Pfitzmann:
  Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation. 310-329
  
• Claus Pahl:
  Interference Analysis for Dependable Systems Using Refinement and Abstraction. 330-349
  
• Neil Henderson, Stephen Paynter:
  The Formal Classification and Verification of Simpson's 4-Slot Asynchronous Communication Mechanism. 350-369
  
• Colin J. Fidge:
  Timing Analysis of Assembler Code Control-Flow Paths. 370-389
  
• María Victoria Cengarle, Alexander Knapp:
  Towards OCL/RT. 390-409
  
• Hubert Garavel, Holger Hermanns:
  On Combining Functional Verification and Performance Evaluation Using CADP. 410-429
  
• David A. Basin:
  The Next 700 Synthesis Calculi. 430
  
• Michael W. Whalen, Johann Schumann, Bernd Fischer:
  Synthesizing Certified Code. 431-450
  
• Augusto Sampaio, Jim Woodcock, Ana Cavalcanti:
  Refinement in Circus. 451-470
  
• Ana Cavalcanti, David A. Naumann:
  Forward Simulation for Data Refinement of Classes. 471-490
  
• Luke Wildman:
  A Formal Basis for a Program Compilation Proof Tool. 491-510
  
• Thomas Firley, Ursula Goltz:
  Property Dependent Abstraction of Control Structure for Software Verification. 511-530
  
• Natalia Ioustinova, Natalia Sidorova, Martin Steffen:
  Closing Open SDL-Systems for Model Checking with DTSpin. 531-548
  
• Lars Michael Kristensen, Thomas Mailund:
  A Generalised Sweep-Line Method for Safety Properties. 549-567
  
• Helen Treharne:
  Supplementing a UML Development Process with B. 568-586
  
• Jin Song Dong, Jing Sun, Hai H. Wang:
  Semantic Web for Extending and Linking Formalisms. 587-606
  
• Takaaki Umedu, Yoshiki Terashima, Keiichi Yasumoto, Akio Nakata, Teruo Higashino, Kenichi Taniguchi:
  A Language for Describing Wireless Mobile Applications with Dynamic Establishment of Multi-way Synchronization Channels. 607-624