5. SEFM 2007: London, England

Keynote Talk

• Michael Jackson:
  Specialising in Software Engineering. 3
  

Software Engineering 1

• David Crocker, Judith Carlton:
  Verification of C Programs Using Automated Reasoning. 7-14
  
• Jon G. Hall, Lucia Rapanotti, Michael Jackson:
  Problem Oriented Software Engineering: A design-theoretic framework for software engineering. 15-24
  
• Ian Bayley:
  Formalising Design Patterns in Predicate Logic. 25-36
  

Mondex/VSI Challenge

• Richard Banach, Czeslaw Jeske, Anthony Hall, Susan Stepney:
  Retrenchment and the Atomicity Pattern. 37-46
  
• Peter H. Schmitt, Isabel Tonin:
  Verifying the Mondex Case Study. 47-58
  

Applications

• Radu Calinescu, Steve Harris, Jeremy Gibbons, Jim Davies, Igor Toujilov, Sylvia B. Nagl:
  Model-driven architecture for cancer research. 59-68
  
• Indranil Saha, Suman Roy, Kuntal Chakraborty:
  Modeling and Verification of TTCAN Startup Protocol Using Synchronous Calendar. 69-79
  
• Prahladavaradan Sampath, A. C. Rajeev, K. C. Shashidhar, S. Ramesh:
  How to Test Program Generators? A Case Study using flex. 80-92
  

Reasoning

• Domagoj Babic, Alan J. Hu, Zvonimir Rakamaric, Byron Cook:
  Proving Termination by Divergence. 93-102
  
• Farhad Mehta:
  Supporting Proof in a Reactive Development Environment. 103-112
  
• Bart Jacobs, Peter Müller, Frank Piessens:
  Sound reasoning about unchecked exceptions. 113-122
  

Keynote Talk

• Patrick Cousot:
  The Rôle of Abstract Interpretation in Formal Methods. 135-140
  

Logics

• Bernhard Beckert, Vladimir Klebanov:
  A Dynamic Logic for Deductive Verification of Concurrent Programs. 141-150
  
• Pablo F. Castro, T. S. E. Maibaum:
  An ought-to-do deontic logic for reasoning about fault-tolerance: the diarrheic philosophers. 151-160
  
• Marius C. Bujorianu, Manuela L. Bujorianu:
  An Integrated Specification Framework for Embedded Systems. 161-172
  

Semantics

• Haitao Dan, Robert M. Hierons, Steve Counsell:
  A Thread-tag Based Semantics for Sequence Diagrams. 173-182
  
• Dima Alhadidi, Nadia Belblidia, Mourad Debbabi, Prabir Bhattacharya:
  An AOP Extended Lambda-Calculus. 183-194
  

Telecommunications

• Holger Grandy, Robert Bertossi, Kurt Stenzel, Wolfgang Reif:
  ASN1-light: A Verified Message Encoding for Security Protocols. 195-204
  
• Manish C. Kumar, K. Gopinath:
  Recovery from DoS Attacks in MIPv6: Modeling and Validation. 205-214
  
• Bernhard K. Aichernig, Bernhard Peischl, Martin Weiglhofer, Franz Wotawa:
  Protocol Conformance Testing a SIP Registrar: an Industrial Application of Formal Methods. 215-226
  

Testing and Model Checking

• Mercedes G. Merayo, Manuel Núñez:
  Testing conformance on Stochastic Stream X-Machines. 227-236
  
• Temesghen Kahsai, Markus Roggenbach, Bernd-Holger Schlingloff:
  Specification-based testing for refinement. 237-246
  
• Neha Rungta, Eric G. Mercer:
  Hardness for Explicit State Software Model Checking Benchmarks. 247-256
  
• Juan Ignacio Perna, Chris George:
  Model Checking RAISE Applicative Specifications. 257-268
  

Keynote Talk

• Byron Cook:
  Automatically Proving Concurrent Programs Correct. 269-272
  

Software Engineering II

• Xianghua Deng, Robby, John Hatcliff:
  Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs. 273-282
  
• Krishna K. Mehra, Sriram K. Rajamani, A. Prasad Sistla, Sumit Kumar Jha:
  Verification of Object Relational Maps. 283-292
  
• K. Lano:
  Formal Specification using Interaction Diagrams. 293-304
  

Services

• Ivan Lanese, Francisco Martins, Vasco Thudichum Vasconcelos, António Ravara:
  Disciplining Orchestration and Conversation in Service-Oriented Computing. 305-314
  
• Huibiao Zhu, Jifeng He, Jing Li, Jonathan P. Bowen:
  Algebraic Approach to Linking the Semantics of Web Services. 315-328
  

Security and Safety

• Dominique Cansell, J. Paul Gibson, Dominique Méry:
  Formal verification of tamper-evident storage for e-voting. 329-338
  
• Robert Colvin, Lindsay Groves:
  A Scalable Lock-Free Stack Algorithm and its Verification. 339-348
  
• Mohamed Saleh, Mourad Debbabi:
  Verifying Security Properties of Cryptoprotocols: A Novel Approach. 349-360
  

Specification and Verification

• Simon Fraser, Richard Banach:
  Configurable Proof Obligations in the Frog Toolkit. 361-370
  
• Steve Reeves, David Streader:
  Feature Refinement. 371-380
  
• Javier Cámara, Gwen Salaün, Carlos Canal:
  Run-time Composition and Adaptation of Mismatching Behavioural Transactions. 381-390
  
• Nabil Hameurlain:
  Flexible Behavioural Compatibility and Substitutability for Component Protocols: A Formal Specification. 391-400