


default search action
5th 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

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-Luminita 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 - Kevin 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 Mostafa 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

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














