FM 2005: Newcastle upon Tyne, UK

John Fitzgerald, Ian J. Hayes, Andrzej Tarlecki (Eds.): FM 2005: Formal Methods, International Symposium of Formal Methods Europe, Newcastle, UK, July 18-22, 2005, Proceedings. Lecture Notes in Computer Science 3582 Springer 2005, ISBN 3-540-27882-6 BibTeX

Keynote Talks

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

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

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

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

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

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

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

Dragan Bosnacki:
On Some Galois Connection Based Abstractions for the Mu-Calculus. 366-381
Electronic Edition (link) BibTeX
Richard Banach, Michael Poppleton, Czeslaw Jeske, Susan Stepney:
Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern. 382-398
Electronic Edition (link) BibTeX
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
Electronic Edition (link) BibTeX

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

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

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