Preface

Committees (PDF)

pp. x

Program Committees (PDF)

pp. xi

Steering Committees (PDF)

pp. xii

Keynote Talk

Specialising in Software Engineering (PDF)

Michael Jackson, Open University

pp. 3

Software Engineering 1

Verification of C Programs Using Automated Reasoning (Abstract)

David Crocker, Escher Technologies Ltd.

Judith Carlton, Escher Technologies Ltd.

pp. 7-14

PDF

Problem Oriented Software Engineering: A design-theoretic framework for software engineering (Abstract)

Jon G. Hall, Open University, UK

Lucia Rapanotti, Open University, UK

Michael Jackson, Open University, UK

pp. 15-24

PDF

Formalising Design Patterns in Predicate Logic (Abstract)

Ian Bayley, Oxford Brookes University

pp. 25-36

PDF

Mondex/VSI Challenge

Retrenchment and the Atomicity Pattern (Abstract)

Richard Banach, University of Manchester

Czeslaw Jeske, University of Manchester

Anthony Hall, Independent Consultant, UK

Susan Stepney, University of York

pp. 37-46

PDF

Verifying the Mondex Case Study (Abstract)

Peter H. Schmitt, Universitat Karlsruhe

Isabel Tonin, Universitat Karlsruhe

pp. 47-58

PDF

Applications

Model-driven architecture for cancer research (Abstract)

Radu Calinescu, University of Oxford

Steve Harris, University of Oxford

Jeremy Gibbons, University of Oxford

Jim Davies, University of Oxford

Igor Toujilov, University College Medical School

Sylvia B. Nagl, University College Medical School

pp. 59-68

PDF

Modeling and Verification of TTCAN Startup Protocol Using Synchronous Calendar (Abstract)

Indranil Saha, HTS(Honeywell Technology Solutions) Research, India

Suman Roy, HTS(Honeywell Technology Solutions) Research, India

Kuntal Chakraborty, Indian Statistical Institute, India

pp. 69-79

PDF

How to Test Program Generators? A Case Study using flex (Abstract)

Prahladavaradan Sampath, General Motors India Science Lab

A. C. Rajeev, General Motors India Science Lab

K. C. Shashidhar, General Motors India Science Lab

S. Ramesh, General Motors India Science Lab

pp. 80-92

PDF

Reasoning

Proving Termination by Divergence. (Abstract)

Domagoj Babic, University of British Columbia

Alan J. Hu, University of British Columbia

Zvonimir Rakamaric, University of British Columbia

Byron Cook, Microsoft Research

pp. 93-102

PDF

Supporting Proof in a Reactive Development Environment (Abstract)

Farhad Mehta, ETH Zurich

pp. 103-112

PDF

Sound reasoning about unchecked exceptions (Abstract)

Bart Jacobs, Katholieke Universiteit Leuven

Peter Muller, Microsoft Research, Redmond

Frank Piessens, Katholieke Universiteit Leuven

pp. 113-122

PDF

The Role of Abstract Interpretation in Formal Methods (PDF)

pp. 135-140

Logics

A Dynamic Logic for Deductive Verification of Concurrent Programs (Abstract)

Bernhard Beckert, University of Koblenz-Landau

Vladimir Klebanov, University of Koblenz-Landau

pp. 141-150

PDF

An ought-to-do deontic logic for reasoning about fault-tolerance: the diarrheic philosophers (Abstract)

Pablo F. Castro, McMaster University

T.S.E. Maibaum, McMaster University

pp. 151-160

PDF

An Integrated Specification Framework for Embedded Systems (Abstract)

Marius C. Bujorianu, University of Kent

Manuela L. Bujorianu, University of Twente

pp. 161-172

PDF

Semantics

A Thread-tag Based Semantics for Sequence Diagrams (Abstract)

Haitao Dan, Brunel University

Robert M. Hierons, Brunel University

Steve Counsell, Brunel University

pp. 173-182

PDF

An AOP Extended Lambda-Calculus (Abstract)

Dima Alhadidi, Concordia University, Canada

Nadia Belblidia, Concordia University, Canada

Mourad Debbabi, Concordia University, Canada

Prabir Bhattacharya, Concordia University, Canada

pp. 183-194

PDF

Telecommunications

ASN1-light: A Verified Message Encoding for Security Protocols (Abstract)

Holger Grandy, Universitat Augsburg

Robert Bertossi, Universitat Augsburg

Kurt Stenzel, Universitat Augsburg

Wolfgang Reif, Universitat Augsburg

pp. 195-204

PDF

Recovery from DoS Attacks in MIPv6: Modeling and Validation (Abstract)

Manish C Kumar, Indian Institute of Science

K Gopinath, Indian Institute of Science

pp. 205-214

PDF

Protocol Conformance Testing a SIP Registrar: an Industrial Application of Formal Methods (Abstract)

Bernhard K. Aichernig, Technische Universitat Graz

Bernhard Peischl, Technische Universitat Graz

Martin Weiglhofer, Technische Universitat Graz

Franz Wotawa, Technische Universitat Graz

pp. 215-226

PDF

Testing and Model Checking

Testing conformance on Stochastic Stream X-Machines (Abstract)

pp. 227-236

PDF

Specification-based testing for refinement (Abstract)

pp. 237-246

PDF

Hardness for Explicit State Software Model Checking Benchmarks (Abstract)

pp. 247-256

PDF

Model Checking RAISE Applicative Specifications (Abstract)

pp. 257-268

PDF

Automatically Proving Concurrent Programs Correct (PDF)

Byron Cook, Microsoft

pp. 269-272

Software Engineering II

Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs (Abstract)

Xianghua Deng, Kansas State University

Robby, Kansas State University

John Hatcliff, Kansas State University

pp. 273-282

PDF

Verification of Object Relational Maps (Abstract)

Krishna K. Mehra, Microsoft Research India

Sriram K. Rajamani, Microsoft Research India

A. Prasad Sistla, University of Illinois at Chicago

Sumit K. Jha, Carnegie Melon University

pp. 283-292

PDF

Formal Specification using Interaction Diagrams (Abstract)

K. Lano

pp. 293-304

PDF

Services

Disciplining Orchestration and Conversation in Service-Oriented Computing (Abstract)

Ivan Lanese, University of Bologna

Francisco Martins, University of Lisbon

Vasco T. Vasconcelos, University of Lisbon

Antonio Ravara, Technical University of Lisbon

pp. 305-314

PDF

Algebraic Approach to Linking the Semantics of Web Services (Abstract)

Huibiao Zhu, East China Normal University

Jifeng He, East China Normal University

Jing Li, East China Normal University

Jonathan P. Bowen, London South Bank University

pp. 315-328

PDF

Security and Safety

Formal verification of tamper-evident storage for e-voting (Abstract)

Dominique Cansell, LORIA & Université de Metz, France

J. Paul Gibson, INT Evry, Paris

Dominique M?ry, Nancy-Universite, Université Henri Poincare Nancy1 & LORIA

pp. 329-338

PDF

A Scalable Lock-Free Stack Algorithm and its Verification (Abstract)

Robert Colvin, University of Queensland, Australia

Lindsay Groves, Victoria University of Wellington, New Zealand

pp. 339-348

PDF

Verifying Security Properties of Cryptoprotocols: A Novel Approach (Abstract)

Mohamed Saleh, Concordia University

Mourad Debbabi, Concordia University

pp. 349-360

PDF

Specification and Verification

Configurable Proof Obligations in the Frog Toolkit (Abstract)

Simon Fraser, University of Manchester

Richard Banach, University of Manchester,

pp. 361-370

PDF

Feature Refinement (Abstract)

Steve Reeves, University of Waikato, Hamilton, New Zealand

David Streader, University of Waikato, Hamilton, New Zealand

pp. 371-380

PDF

Run-time Composition and Adaptation of Mismatching Behavioural Transactions (Abstract)

Javier Camara, University of Malaga, Spain

Gwen Salaun, University of Malaga, Spain

Carlos Canal, University of Malaga, Spain

pp. 381-390

PDF

Flexible Behavioural Compatibility and Substitutability for Component Protocols: A Formal Specification (Abstract)

Nabil Hameurlain, LIUPPA Laboratory, University of Pau, France

pp. 391-400

PDF

Author Index

Author Index (PDF)

pp. 401