FM 2005: Newcastle upon Tyne, UK

Keynote Talks

• Mathai Joseph:
  Formal Aids for the Growth of Software Systems. 1
  
• Marie-Claude Gaudel:
  Formal Methods and Testing: Hypotheses, and Correctness Approximations. 2-8
  
• C. W. Johnson:
  The Natural History of Bugs: Using Formal Methods to Analyse Software Related Failures in Space Missions. 9-25
  

Object Orientation

• K. Rustan M. Leino, Peter Müller:
  Modular Verification of Static Class Invariants. 26-42
  
• Ioannis T. Kassios:
  Decoupling in Object Orientation. 43-58
  
• Cees Pierik, Dave Clarke, Frank S. de Boer:
  Controlling Object Allocation Using Creation Guards. 59-74
  
• Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard, Mark Utting:
  Symbolic Animation of JML Specifications. 75-90
  

Resource Analysis and Verification

• David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider:
  Certified Memory Usage Analysis. 91-106
  
• Orieta Celiku, Annabelle McIver:
  Compositional Specification and Analysis of Cost-Based Properties in Probabilistic Programs. 107-122
  
• Pierre Salverda, Grigore Rosu, Craig B. Zilles:
  Formally Defining and Verifying Master/Slave Speculative Parallelization. 123-138
  

Timing and Testing

• Martin De Wulf, Laurent Doyen, Jean-François Raskin:
  Systematic Implementation of Real-Time Models. 139-156
  
• Alan Wassyng, Mark Lawford, Xiayong Hu:
  Timing Tolerances in Safety-Critical Software. 157-172
  
• Henrik C. Bohnenkamp, Axel Belinfante:
  Timed Testing with TorX. 173-188
  
• Vlad Rusu, Hervé Marchand, Thierry Jéron:
  Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems. 189-204
  

CSP, B and Circus

• Christie Bolton:
  Adding Conflict and Confusion to CSP. 205-220
  
• Michael J. Butler, Michael Leuschel:
  Combining CSP and B for Specification and Property Verification. 221-236
  
• Jim Woodcock, Ana Cavalcanti, Leonardo Freitas:
  Operational Semantics for Model Checking Circus. 237-252
  
• Ana Cavalcanti, Phil Clayton, Colin O'Halloran:
  Control Law Diagrams in Circus. 253-268
  

Security

• David A. Basin, Hironobu Kuruma, Kazuo Takaragi, Burkhart Wolff:
  Verification of a Signature Architecture with HOL-Z. 269-285
  
• Mikael Buchholtz, Stephen Gilmore, Valentin Haenel, Carlo Montangero:
  End-to-End Integrated Security and Performance Analysis on the DEGAS Choreographer Platform. 286-301
  
• June Andronick, Boutheina Chetali, Christine Paulin-Mohring:
  Formal Verification of Security Properties of Smart Card Embedded Source Code. 302-317
  

Networks and Processes

• Pamela Zave:
  A Formal Model of Addressing for Interoperating Networks. 318-333
  
• Yu Lei, S. Purushothaman Iyer:
  An Approach to Unfolding Asynchronous Communication Protocols. 334-349
  
• Zongyan Qiu, Shuling Wang, Geguang Pu, Xiangpeng Zhao:
  Semantics of BPEL4WS-Like Fault and Compensation Handling. 350-365
  

Abstraction, Retrenchment and Rewriting

• Dragan Bosnacki:
  On Some Galois Connection Based Abstractions for the Mu-Calculus. 366-381
  
• Richard Banach, Michael Poppleton, Czeslaw Jeske, Susan Stepney:
  Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern. 382-398
  
• Tiago L. Alves, Paulo F. Silva, Joost Visser, José Nuno Oliveira:
  Strategic Term Rewriting and Its Application to a VDMSL to SQL Conversion. 399-414
  

Scenarios and Modeling Languages

• Jun Sun, Jin Song Dong:
  Synthesis of Distributed Processes from Scenario-Based Specifications. 415-431
  
• Emilia Katz, Shmuel Katz:
  Verifying Scenario-Based Aspect Specifications. 432-447
  
• Soon-Kyeong Kim, Damian Burger, David A. Carrington:
  An MDA Approach Towards Integrating Formal and Informal Modeling Languages. 448-464
  

Model Checking

• Jochen Hoenicke, Patrick Maier:
  Model-Checking of Specifications Integrating Processes, Data and Time. 465-480
  
• Alastair F. Donaldson, Alice Miller:
  Automatic Symmetry Detection for Model Checking Using Computational Group Theory. 481-496
  
• Subramanian K. Iyer, Debashis Sahoo, E. Allen Emerson, Jawahar Jain:
  On Partitioning and Symbolic Model Checking. 497-511
  
• Natasha Sharygina, Sagar Chaki, Edmund M. Clarke, Nishant Sinha:
  Dynamic Component Substitutability Analysis. 512-528
  

Industry Day: Abstracts of Invited Talks

• John Harrison:
  Floating-Point Verification. 529-532
  
• Stefan Eisler, Christian Scheidler, Bernhard Josko, Guido Sandmann, Joachim Stroop:
  Preliminary Results of a Case Study: Model Checking for Advanced Automotive Applications. 533-536
  
• Alexander Pretschner:
  Model-Based Testing in Practice. 537-541
  
• Colin Campbell, Wolfgang Grieskamp, Lev Nachmanson, Wolfram Schulte, Nikolai Tillmann, Margus Veanes:
  Testing Concurrent Object-Oriented Systems with Spec Explorer. 542-547
  
• Guy H. Broadfoot:
  ASD Case Notes: Costs and Benefits of Applying Formal Methods to Industrial Control Software. 548-551
  
• Gerrit Muller:
  The Informal Nature of Systems Engineering. 552-556