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 Müller, 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 Núñez
- 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 Méry
- 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 Salaün, and Carlos Canal
- Flexible Behavioural Compatibility and Substitutability
for Component Protocols: A Formal Specification
- Nabil Hameurlain
- 18:00 Closing Remarks
|
