FME 2002: Formal Methods - Getting IT Right

Little Engines of Proof.- Automated Boundary Testing from Z and B.- Improvements in Coverability Analysis.- Heuristic-Driven Test Case Selection from Formal Specifications. A Case Study.- UniTesK Test Suite Architecture.- Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited.- Do Not Read This.- Safeness of Make-Based Incremental Recompilation.- An Algorithmic Approach to Design Exploration.- Mechanical Abstraction of CSP Z Processes.- Verifying Erlang Code: A Resource Locker Case-Study.- Towards an Integrated Model Checker for Railway Signalling Data.- Correctness by Construction: Integrating Formality into a Commercial Development Process.- VAlloy - Virtual Functions Meet a Relational Language.- Verification Using Test Generation Techniques.- Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java.- Development of an Embedded Verifier for Java Card Byte Code Using Formal Methods.- Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation.- Interference Analysis for Dependable Systems Using Refinement and Abstraction.- The Formal Classification and Verification of Simpson's 4-Slot Asynchronous Communication Mechanism.- Timing Analysis of Assembler Code Control-Flow Paths.- Towards OCL/RT.- On Combining Functional Verification and Performance Evaluation Using CADP.- The Next 700 Synthesis Calculi.- Synthesizing Certified Code.- Refinement in Circus.- Forward Simulation for Data Refinement of Classes.- A Formal Basis for a Program Compilation Proof Tool.- Property Dependent Abstraction of Control Structure for Software Verification.- Closing Open SDL-Systems for Model Checking with DTSpin.- A Generalised Sweep-Line Method for Safety Properties.- Supplementing a UML Development Process with B.- Semantic Web for Extending and Linking Formalisms.- A Language for Describing Wireless Mobile Applications with Dynamic Establishment of Multi-way Synchronization