The Community for Technology Leaders
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05) (2007)
London, England
Sept. 10, 2007 to Sept. 14, 2007
ISBN: 0-7695-2884-8
TABLE OF CONTENTS
Introduction

Preface (PDF)

pp. ix

Committees (PDF)

pp. x
Keynote Talk
Software Engineering 1

Verification of C Programs Using Automated Reasoning (Abstract)

Judith Carlton , Escher Technologies Ltd.
David Crocker , Escher Technologies Ltd.
pp. 7-14

Formalising Design Patterns in Predicate Logic (Abstract)

Ian Bayley , Oxford Brookes University
pp. 25-36
Mondex/VSI Challenge

Retrenchment and the Atomicity Pattern (Abstract)

Richard Banach , University of Manchester
Czeslaw Jeske , University of Manchester
Susan Stepney , University of York
Anthony Hall , Independent Consultant, UK
pp. 37-46

Verifying the Mondex Case Study (Abstract)

Peter H. Schmitt , Universitat Karlsruhe
Isabel Tonin , Universitat Karlsruhe
pp. 47-58
Applications

Model-driven architecture for cancer research (Abstract)

Steve Harris , University of Oxford
Jeremy Gibbons , University of Oxford
Igor Toujilov , University College Medical School
Jim Davies , University of Oxford
Sylvia B. Nagl , University College Medical School
Radu Calinescu , University of Oxford
pp. 59-68

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

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

Prahladavaradan Sampath , General Motors India Science Lab
S. Ramesh , General Motors India Science Lab
K. C. Shashidhar , General Motors India Science Lab
A. C. Rajeev , General Motors India Science Lab
pp. 80-92
Reasoning

Proving Termination by Divergence. (Abstract)

Domagoj Babic , University of British Columbia
Zvonimir Rakamaric , University of British Columbia
Alan J. Hu , University of British Columbia
Byron Cook , Microsoft Research
pp. 93-102

Sound reasoning about unchecked exceptions (Abstract)

Bart Jacobs , Katholieke Universiteit Leuven
Peter Muller , Microsoft Research, Redmond
Frank Piessens , Katholieke Universiteit Leuven
pp. 113-122
Keynote Talk
Logics

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

Vladimir Klebanov , University of Koblenz-Landau
Bernhard Beckert , University of Koblenz-Landau
pp. 141-150

An Integrated Specification Framework for Embedded Systems (Abstract)

Manuela L. Bujorianu , University of Twente
Marius C. Bujorianu , University of Kent
pp. 161-172
Semantics

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

Steve Counsell , Brunel University
Robert M. Hierons , Brunel University
Haitao Dan , Brunel University
pp. 173-182

An AOP Extended Lambda-Calculus (Abstract)

Prabir Bhattacharya , Concordia University, Canada
Mourad Debbabi , Concordia University, Canada
Dima Alhadidi , Concordia University, Canada
Nadia Belblidia , Concordia University, Canada
pp. 183-194
Telecommunications

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

Holger Grandy , Universitat Augsburg
Wolfgang Reif , Universitat Augsburg
Robert Bertossi , Universitat Augsburg
Kurt Stenzel , Universitat Augsburg
pp. 195-204

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

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

Martin Weiglhofer , Technische Universitat Graz
Bernhard Peischl , Technische Universitat Graz
Bernhard K. Aichernig , Technische Universitat Graz
Franz Wotawa , Technische Universitat Graz
pp. 215-226
Testing and Model Checking
Keynote Talk
Software Engineering II

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

Xianghua Deng , Kansas State University
John Hatcliff , Kansas State University
Robby , Kansas State University
pp. 273-282

Verification of Object Relational Maps (Abstract)

A. Prasad Sistla , University of Illinois at Chicago
Sumit K. Jha , Carnegie Melon University
Krishna K. Mehra , Microsoft Research India
Sriram K. Rajamani , Microsoft Research India
pp. 283-292
Services

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

Antonio Ravara , Technical University of Lisbon
Ivan Lanese , University of Bologna
Vasco T. Vasconcelos , University of Lisbon
Francisco Martins , University of Lisbon
pp. 305-314

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

Jifeng He , East China Normal University
Huibiao Zhu , East China Normal University
Jonathan P. Bowen , London South Bank University
Jing Li , East China Normal University
pp. 315-328
Security and Safety

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

Dominique M?ry , Nancy-Universite, Université Henri Poincare Nancy1 & LORIA
Dominique Cansell , LORIA & Université de Metz, France
J. Paul Gibson , INT Evry, Paris
pp. 329-338

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

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

Mourad Debbabi , Concordia University
Mohamed Saleh , Concordia University
pp. 349-360
Specification and Verification

Configurable Proof Obligations in the Frog Toolkit (Abstract)

Richard Banach , University of Manchester,
Simon Fraser , University of Manchester
pp. 361-370

Feature Refinement (Abstract)

David Streader , University of Waikato, Hamilton, New Zealand
Steve Reeves , University of Waikato, Hamilton, New Zealand
pp. 371-380

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
Author Index

Author Index (PDF)

pp. 401
101 ms
(Ver )