5. SEFM 2007: London, England

Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 10-14 September 2007, London, England, UK. IEEE Computer Society 2007, ISBN 978-0-7695-2884-7 BibTeX

Keynote Talk

Michael Jackson:
Specialising in Software Engineering. 3
Electronic Edition (link) BibTeX

Software Engineering 1

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

Mondex/VSI Challenge

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

Applications

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

Reasoning

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

Keynote Talk

Patrick Cousot:
The Rôle of Abstract Interpretation in Formal Methods. 135-140
Electronic Edition (link) BibTeX

Logics

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

Semantics

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

Telecommunications

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

Testing and Model Checking

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

Keynote Talk

Byron Cook:
Automatically Proving Concurrent Programs Correct. 269-272
Electronic Edition (link) BibTeX

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
Electronic Edition (link) BibTeX
Krishna K. Mehra, Sriram K. Rajamani, A. Prasad Sistla, Sumit Kumar Jha:
Verification of Object Relational Maps. 283-292
Electronic Edition (link) BibTeX
K. Lano:
Formal Specification using Interaction Diagrams. 293-304
Electronic Edition (link) BibTeX

Services

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

Security and Safety

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

Specification and Verification

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