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

Preface (PDF)

pp. ix

Committees (PDF)

pp. x
Keynote Talk
Software Engineering 1

Verification of C Programs Using Automated Reasoning (Abstract)

David Crocker , Escher Technologies Ltd.
Judith Carlton , 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
Anthony Hall , Independent Consultant, UK
Susan Stepney , University of York
pp. 37-46

Verifying the Mondex Case Study (Abstract)

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

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

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

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

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

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

An Integrated Specification Framework for Embedded Systems (Abstract)

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

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

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

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

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)

Bernhard K. Aichernig , Technische Universitat Graz
Bernhard Peischl , Technische Universitat Graz
Martin Weiglhofer , 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
Robby , Kansas State University
John Hatcliff , Kansas State University
pp. 273-282

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

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

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

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)

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

Configurable Proof Obligations in the Frog Toolkit (Abstract)

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

Feature Refinement (Abstract)

Steve Reeves , University of Waikato, Hamilton, New Zealand
David Streader , 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
92 ms
(Ver 3.3 (11022016))