FM 2005: Formal Methods: International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings (Paperback, 2005)

Keynote Talks.- Formal Aids for the Growth of Software Systems.- Formal Methods and Testing: Hypotheses, and Correctness Approximations.- The Natural History of Bugs: Using Formal Methods to Analyse Software Related Failures in Space Missions.- Object Orientation.- Modular Verification of Static Class Invariants.- Decoupling in Object Orientation.- Controlling Object Allocation Using Creation Guards.- Symbolic Animation of JML Specifications.- Resource Analysis and Verification.- Certified Memory Usage Analysis.- Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs.- Formally Defining and Verifying Master/Slave Speculative Parallelization.- Timing and Testing.- Systematic Implementation of Real-Time Models.- Timing Tolerances in Safety-Critical Software.- Timed Testing with TorX.- Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems.- CSP, B and Circus.- Adding Conflict and Confusion to CSP.- Combining CSP and B for Specification and Property Verification.- Operational Semantics for Model Checking Circus.- Control Law Diagrams in Circus.- Security.- Verification of a Signature Architecture with HOL-Z.- End-to-End Integrated Security and Performance Analysis on the DEGAS Choreographer Platform.- Formal Verification of Security Properties of Smart Card Embedded Source Code.- Networks and Processes.- A Formal Model of Addressing for Interoperating Networks.- An Approach to Unfolding Asynchronous Communication Protocols.- Semantics of BPEL4WS-Like Fault and Compensation Handling.- Abstraction, Retrenchment and Rewriting.- On Some Galois Connection Based Abstractions for the Mu-Calculus.- Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern.- Strategic Term Rewriting and Its Application to a Vdm-sl to Sql Conversion.- Scenarios and Modeling Languages.- Synthesis of Distributed Processes from Scenario-Based Specifications.- Verifying Scenario-Based Aspect Specifications.- An MDA Approach Towards Integrating Formal and Informal Modeling Languages.- Model Checking.- Model-Checking of Specifications Integrating Processes, Data and Time.- Automatic Symmetry Detection for Model Checking Using Computational Group Theory.- On Partitioning and Symbolic Model Checking.- Dynamic Component Substitutability Analysis.- Industry Day: Abstracts of Invited Talks.- Floating-Point Verification.- Preliminary Results of a Case Study: Model Checking for Advanced Automotive Applications.- Model-Based Testing in Practice.- Testing Concurrent Object-Oriented Systems with Spec Explorer.- ASD Case Notes: Costs and Benefits of Applying Formal Methods to Industrial Control Software.- The Informal Nature of Systems Engineering.