FME 2003: Formal Methods

Invited Speakers.- Looking Back to the Future.- Past, Present, and Future of SRA Implementation of CafeOBJ.- On Failures and Faults.- Trends in Software Verification.- Event Based Sequential Program Development: Application to Constructing a Pointer Program.- I-Day.- Proving the Shalls.- Adaptable Translator of B Specifications to Embedded C Programs.- Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle.- Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project.- Control Systems and Industrial Applications.- Determining the Specification of a Control System from That of Its Environment.- Managerial Issues for the Consideration and Use of Formal Methods.- Verifying Emulation of Legacy Mission Computer Systems.- Improving Safety Assessment of Complex Systems: An Industrial Case Study.- Communications System Verification.- Compositional Verification of an ATM Protocol.- Proving the Correctness of Simpson's 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method.- Synthesis and Verification of Constraints in the PGM Protocol.- Co-specification and Compilers.- Mapping Statecharts to Verilog for Hardware/Software Co-specification.- A Strategy for Compiling Classes, Inheritance, and Dynamic Binding.- Composition.- A Semantic Foundation for TCOZ in Unifying Theories of Programming.- Refinement and Verification of Synchronized Component-Based Systems.- Certifying and Synthesizing Membership Equational Proofs.- Team Automata Satisfying Compositionality.- Composing Invariants.- Java, Object Orientation and Modularity.- Java Applet Correctness: A Developer-Oriented Approach.- Improving JML: For a Safer and More Effective Language.- Using Abstractions for Heuristic State Space Exploration of ReactiveObject-Oriented Systems.- A Formal Framework for Modular Synchronous System Design.- Model Checking.- Generating Counterexamples for Multi-valued Model-Checking.- Combining Real-Time Model-Checking and Fault Tree Analysis.- Model-Checking TRIO Specifications in SPIN.- Computing Meta-transitions for Linear Transition Systems with Polynomials.- Translation-Based Compositional Reasoning for Software Systems.- Watchdog Transformations for Property-Oriented Model-Checking.- Parallel Process.- A Circus Semantics for Ravenscar Protected Objects.- Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach.- A General Approach to Deadlock Freedom Verification for Software Architectures.- Taking Alloy to the Movies.- Interacting State Machines for Mobility.- Composing Temporal-Logic Specifications with Machine Assistance.- Program Checking and Testing.- Model Checking FTA.- Program Checking with Certificates: Separating Correctness-Critical Code.- Reification of Executable Test Scripts in Formal Specification-Based Test Generation: The Java Card Transaction Mechanism Case Study.- Checking and Reasoning about Semantic Web through Alloy.- B Method.- Structuring Retrenchments in B by Decomposition.- Design of an Automatic Prover Dedicated to the Refinement of Database Applications.- ProB: A Model Checker for B.- Security.- SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis.- Correctness of Source-Level Safety Policies.- A Topological Characterization of TCP/IP Security.