FME 2003: Pisa, Italy

Invited Speakers

• Kouichi Kishida:
  Looking Back to the Future: Thoughts on Paradigm Shift in Software Development. 1-6
  
• Toshimi Sawada, Kouichi Kishida, Kokichi Futatsugi:
  Past, Present, and Future of SRA Implementation of CafeOBJ: Annex. 7-17
  
• Brian Randell:
  On Failures and Faults. 18-39
  
• Gerard J. Holzmann:
  Trends in Software Verification. 40-50
  
• Jean-Raymond Abrial:
  Event Based Sequential Program Development: Application to Constructing a Pointer Program. 51-74
  

I-Day

• Steven P. Miller, Alan C. Tribble, Mats Per Erik Heimdahl:
  Proving the Shalls. 75-93
  
• Didier Bert, Sylvain Boulmé, Marie-Laure Potet, Antoine Requet, Laurent Voisin:
  Adaptable Translator of B Specifications to Embedded C Programs. 94-113
  
• Daniele Compare, Paola Inverardi, Patrizio Pelliccione, Alessandra Sebastiani:
  Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle. 114-132
  
• Alan Wassyng, Mark Lawford:
  Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project. 133-153
  

Control Systems and Industrial Applications

• Ian J. Hayes, Michael A. Jackson, Cliff B. Jones:
  Determining the Specification of a Control System from That of Its Environment. 154-169
  
• Donna C. Stidolph, E. James Whitehead Jr.:
  Managerial Issues for the Consideration and Use of Formal Methods. 170-186
  
• Colin J. Fidge:
  Verifying Emulation of Legacy Mission Computer Systems. 187-207
  
• Marco Bozzano, Antonella Cavallo, Massimo Cifaldi, Laura Valacca, Adolfo Villafiorita:
  Improving Safety Assessment of Complex Systems: An Industrial Case Study. 208-222
  

Communications System Verification

• Vlad Rusu:
  Compositional Verification of an ATM Protocol. 223-243
  
• Neil Henderson:
  Proving the Correctness of Simpson's 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method. 244-263
  
• Marc Boyer, Mihaela Sighireanu:
  Synthesis and Verification of Constraints in the PGM Protocol. 264-281
  

Co-specification and Compilers

• Shengchao Qin, Wei-Ngan Chin:
  Mapping Statecharts to Verilog for Hardware/Software Co-specification. 282-300
  
• Adolfo Duran, Ana Cavalcanti, Augusto Sampaio:
  A Strategy for Compiling Classes, Inheritance, and Dynamic Binding. 301-320
  

Composition

• Shengchao Qin, Jin Song Dong, Wei-Ngan Chin:
  A Semantic Foundation for TCOZ in Unifying Theories of Programming. 321-340
  
• Olga Kouchnarenko, Arnaud Lanoix:
  Refinement and Verification of Synchronized Component-Based Systems. 341-358
  
• Grigore Rosu, Steven Eker, Patrick Lincoln, José Meseguer:
  Certifying and Synthesizing Membership Equational Proofs. 359-380
  
• Maurice H. ter Beek, Jetty Kleijn:
  Team Automata Satisfying Compositionality. 381-400
  
• Michel Charpentier:
  Composing Invariants. 401-421
  

Java, Object Orientation and Modularity

• Lilian Burdy, Antoine Requet, Jean-Louis Lanet:
  Java Applet Correctness: A Developer-Oriented Approach. 422-439
  
• Patrice Chalin:
  Improving JML: For a Safer and More Effective Language. 440-461
  
• Marc Lettrari:
  Using Abstractions for Heuristic State Space Exploration of Reactive Object-Oriented Systems. 462-481
  
• Maria-Cristina V. Marinescu, Martin C. Rinard:
  A Formal Framework for Modular Synchronous System Design. 482-502
  

Model Checking

• Arie Gurfinkel, Marsha Chechik:
  Generating Counterexamples for Multi-valued Model-Checking. 503-521
  
• Andreas Schäfer:
  Combining Real-Time Model-Checking and Fault Tree Analysis. 522-541
  
• Angelo Morzenti, Matteo Pradella, Pierluigi San Pietro, Paola Spoletini:
  Model-Checking TRIO Specifications in SPIN. 542-561
  
• Julien Musset, Michaël Rusinowitch:
  Computing Meta-transitions for Linear Transition Systems with Polynomials. 562-581
  
• Fei Xie, James C. Browne, Robert P. Kurshan:
  Translation-Based Compositional Reasoning for Software Systems. 582-599
  
• Michael Goldsmith, Nick Moffat, Bill Roscoe, Tim Whitworth, Irfan Zakiuddin:
  Watchdog Transformations for Property-Oriented Model-Checking. 600-616
  

Parallel Process

• Diyaa-Addein Atiya, Steve King, Jim Woodcock:
  A Circus Semantics for Ravenscar Protected Objects. 617-635
  
• Pascal Fenkam, Harald Gall, Mehdi Jazayeri:
  Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach. 636-657
  
• Alessandro Aldini, Marco Bernardo:
  A General Approach to Deadlock Freedom Verification for Software Architectures. 658-677
  
• Marcelo F. Frias, Carlos López Pombo, Gabriel Baum, Nazareno Aguirre, T. S. E. Maibaum:
  Taking Alloy to the Movies. 678-697
  
• Thomas A. Kuhn, David von Oheimb:
  Interacting State Machines for Mobility. 698-718
  
• Jei-Wen Teng, Yih-Kuen Tsay:
  Composing Temporal-Logic Specifications with Machine Assistance. 719-738
  

Program Checking and Testing

• Andreas Thums, Gerhard Schellhorn:
  Model Checking FTA. 739-757
  
• Sabine Glesner:
  Program Checking with Certificates: Separating Correctness-Critical Code. 758-777
  
• Fabrice Bouquet, Bruno Legeard:
  Reification of Executable Test Scripts in Formal Specicifation-Based Test Generation: The Java Card Transaction Mechanism Case Study. 778-795
  
• Jin Song Dong, Jing Sun, Hai H. Wang:
  Checking and Reasoning about Semantic Web through Alloy. 796-813
  

B Method

• Michael Poppleton, Richard Banach:
  Structuring Retrenchments in B by Decomposition. 814-833
  
• Amel Mammar, Régine Laleau:
  Design of an Automatic Prover Dedicated to the Refinement of Database Applications. 834-854
  
• Michael Leuschel, Michael J. Butler:
  ProB: A Model Checker for B. 855-874
  

Security

• Alessandro Armando, Luca Compagna, Pierre Ganty:
  SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis. 875-893
  
• Ewen Denney, Bernd Fischer:
  Correctness of Source-Level Safety Policies. 894-913
  
• Giovanni Vigna:
  A Topological Characterization of TCP/IP Security. 914-939