SEFM 2007
5th IEEE International Conference on
Software Engineering and Formal Methods
London, UK
September 10-14, 2007


Tuesday 11 Sep


Wednesday 12 Sep

Thursday 13 Sep

Friday 14 Sep

Tuesday 11 September 2007 (Tutorials)

09:00 Tutorial I (Part 1)

Model-checking in Human-computer Interaction (Part 1)
Antonio Cerone, UNU-IIST, Macau SAR China

11:00 Break

11:30 Tutorial I (Part 2)

Model-checking in Human-computer Interaction (Part 2)
Antonio Cerone, UNU-IIST, Macau SAR China

13:00 Lunch

14:00 Tutorial II and III (Part 1)

Retrenchment (Part 1)
Richard Banach, University of Manchester, UK

Formal Methods for Service-oriented Systems (Part 1)
José Luiz Fiadeiro, University of Leicester, UK

16:00 Break

16:30 Tutorial II and III (Part 2)

Retrenchment (Part 2)
Richard Banach, University of Manchester, UK

Formal Methods for Service-oriented Systems (Part 2)
José Luiz Fiadeiro, University of Leicester, UK

Wednesday 12 September 2007

08:00 Registration

08:45 Opening

9:00 Keynote Talk

Specializing in Software Engineering
Michael Jackson, The Open University

10:15 Software Engineering 1

Verification of C Programs Using Automated Reasoning
David Crocker and Judith Carlton

Problem Oriented Software Engineering: A Design-Theoretic Framework for Software Engineering
Jon G. Hall, Lucia Rapanotti, and Michael Jackson

Formalising Design Patterns in Predicate Logic
Ian Bayley and Hong Zhu

11:45 Break

12:00 Mondex/VSI Challenge

Retrenchment and the Atomicity Pattern
Richard Banach, Czeslaw Jeske, Anthony Hall, and Susan Stepney

Verifying the Mondex Case Study
Peter H. Schmitt and Isabel Tonin

13:00 Lunch

14:00 Applications

Model-Driven Architecture for Cancer research
Radu Calinescu, Steve Harris, Jeremy Gibbons, Jim Davies, Igor Toujilov, and Sylvia B. Nagl

Modeling and Verification of TTCAN Startup Protocol Using Synchronous Calendar
Indranil Saha, Suman Roy, and Kuntal Chakraborty

How to Test Program Generators? A Case Study Using flex
Prahladavaradan Sampath, A.C. Rajeev, K.C. Shashidhar, and S. Ramesh

15:30 Break

16:00 Reasoning

Proving Termination by Divergence
Domagoj Babi, Alan J. Hu, Zvonimir Rakamari, and Byron Cook

Supporting Proof in a Reactive Development Environment
Farhad Mehta

Sound Reasoning about Unchecked Exceptions
Bart Jacobs, Peter Mller, and Frank Piessens

Reasoning about Linear Systems
Rob Arthan, Ursula Martin, Erik Arne Mathiesen, and Paulo Oliva

Thursday 13 September 2007

9:00 Keynote Talk

The Role of Abstract Interpretation in Formal Methods
Patrick Cousot, ENS

10:15 Logics

A Dynamic Logic for Deductive Verification of Concurrent Programs
Bernhard Beckert and Vladimir Klebanov

An Ought-to-Do Deontic Logic for Reasoning about Fault-Tolerance: The Diarrheic Philosophers
Pablo F. Castro and Tom S.E. Maibaum

An Integrated Specification Framework for Embedded Systems
Marius C. Bujorianu and Manuela L. Bujorianu

11:45 Break

12:15 Semantics

A Thread-Tag Based Semantics for Sequence Diagrams
Haitao Dan, Robert M. Hierons, and Steve Counsell

Lambda_AOP: An AOP Extended Lambda-Calculus
Dima Alhadidi, Nadia Belblidia, Mourad Debbabi, and Prabir Bhattacharya

13:00 Lunch

14:00 Telecommunications

ASN1-light: A Verified Message Encoding for Security Protocols
Holger Grandy, Robert Bertossi, Kurt Stenzel, and Wolfgang Reif

Recovery from DoS Attacks in MIPv6: Modeling and Validation
Manish Kumar C. and K. Gopinath

Protocol Conformance Testing a SIP Registrar: An Industrial Application of Formal Methods
Bernhard K. Aichernig, Bernhard Peischl, Martin Weiglhofer, and Franz Wotawa

15:30 Break

16:00 Testing and Model Checking

Testing Conformance on Stochastic Stream X-Machines
Mercedes G. Merayo and Manuel Nez

Specification-Based Testing for Refinement
Temesghen Kahsai, Markus Roggenbach, and Bernd-Holger Schlingloff

Hardness for Explicit State Software Model Checking Benchmarks
Neha Rungta and Eric G. Mercer

Model Checking RAISE Applicative Specifications
Juan Ignacio Perna and Chris George

Friday 14 September 2007

09:00 Keynote Talk

Automatically Proving Concurrent Programs Correct
Byron Cook, Microsoft

10:15 Software Engineering II

Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs
Xianghua Deng, Robby, and John Hatcliff

Verification of Object Relational Maps
Krishna K. Mehra, Sriram K. Rajamani, A. Prasad Sistla, and Sumit K. Jha

Formal Specification Using Interaction Diagrams
Kevin Lano

11:45 Break

12:00 Services

Disciplining Orchestration and Conversation in Service-Oriented Computing
Ivan Lanese, Vasco T. Vasconcelos, Francisco Martins, and António Ravara

Algebraic Approach to Linking the Semantics of Web Services
Huibiao Zhu, Jifeng He, Jing Li, and Jonathan P. Bowen

13:00 Lunch

14:00 Security and Safety

Formal Verification of tamper-evident Storage for e-Voting
Dominique Cansell, J. Paul Gibson, and Dominique Mry

A Scalable Lock-Free Stack Algorithm and its Verification
Robert Colvin and Lindsay Groves

Verifying Security Properties of Cryptoprotocols: A Novel Approach
Mohamed Saleh and Mourad Debbabi

15:30 Break

16:00 Specification and Verification

Configurable Proof Obligations in the Frog Toolkit
Simon Fraser and Richard Banach

Feature Refinement
David Streader and Steve Reeves

Run-Time Composition and Adaptation of Mismatching Behavioural Transactions
Javier Cámara, Gwen Salan, and Carlos Canal

Flexible Behavioural Compatibility and Substitutability for Component Protocols: A Formal Specification
Nabil Hameurlain

18:00 Closing Remarks