Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods
SEFM, 2007.

@proceedings{SEFM-2007,
	address       = "England, United Kingdom",
	ee            = "http://www.computer.org/csdl/proceedings/sefm/2007/2884/00/index.html",
	isbn          = "978-0-7695-2884-7",
	publisher     = "{IEEE Computer Society}",
	title         = "{Proceedings of the Fifth IEEE International Conference on Software Engineering and Formal Methods}",
	year          = 2007,
}

Contents (38 items)

8 ×#verification
4 ×#protocol
4 ×#proving
4 ×#source code
4 ×#specification
4 ×#using
3 ×#formal method
3 ×#logic
3 ×#modelling
3 ×#reasoning

SEFM-2007-Jackson #re-engineering

Specialising in Software Engineering (MJ), p. 3.

SEFM-2007-CrockerC #automation #c #reasoning #source code #using #verification

Verification of C Programs Using Automated Reasoning (DC, JC), pp. 7–14.

SEFM-2007-HallRJ #framework #problem #re-engineering

Problem Oriented Software Engineering: A design-theoretic framework for software engineering (JGH, LR, MJ), pp. 15–24.

SEFM-2007-Bayley #design pattern #formal method #logic

Formalising Design Patterns in Predicate Logic (IB), pp. 25–36.

SEFM-2007-BanachJHS

Retrenchment and the Atomicity Pattern (RB, CJ, AH, SS), pp. 37–46.

SEFM-2007-SchmittT #case study #verification

Verifying the Mondex Case Study (PHS, IT), pp. 47–58.

SEFM-2007-CalinescuHGDTN #architecture #modelling #research

Model-driven architecture for cancer research (RC, SH, JG, JD, IT, SBN), pp. 59–68.

SEFM-2007-SahaRC #modelling #protocol #using #verification

Modeling and Verification of TTCAN Startup Protocol Using Synchronous Calendar (IS, SR, KC), pp. 69–79.

SEFM-2007-SampathRSR #case study #generative #how #using

How to Test Program Generators? A Case Study using flex (PS, ACR, KCS, SR), pp. 80–92.

SEFM-2007-BabicHRC #proving #termination

Proving Termination by Divergence (DB, AJH, ZR, BC), pp. 93–102.

SEFM-2007-Mehta #development #proving

Supporting Proof in a Reactive Development Environment (FM), pp. 103–112.

SEFM-2007-JacobsMP #exception #reasoning

Sound reasoning about unchecked exceptions (BJ, PM, FP), pp. 113–122.

SEFM-2007-Cousot #abstract interpretation #formal method

The Rôle of Abstract Interpretation in Formal Methods (PC), pp. 135–140.

SEFM-2007-BeckertK #concurrent #deduction #logic #source code #verification

A Dynamic Logic for Deductive Verification of Concurrent Programs (BB, VK), pp. 141–150.

SEFM-2007-CastroM #fault tolerance #logic #reasoning

An ought-to-do deontic logic for reasoning about fault-tolerance: the diarrheic philosophers (PFC, TSEM), pp. 151–160.

SEFM-2007-BujorianuB #embedded #framework #specification

An Integrated Specification Framework for Embedded Systems (MCB, MLB), pp. 161–172.

SEFM-2007-DanHC #diagrams #semantics #sequence chart #thread

A Thread-tag Based Semantics for Sequence Diagrams (HD, RMH, SC), pp. 173–182.

SEFM-2007-AlhadidiBDB #aspect-oriented #λ-calculus

An AOP Extended λ-Calculus (DA, NB, MD, PB), pp. 183–194.

SEFM-2007-GrandyBSR #encoding #named #protocol #security

ASN1-light: A Verified Message Encoding for Security Protocols (HG, RB, KS, WR), pp. 195–204.

SEFM-2007-KumarG #modelling #validation

Recovery from DoS Attacks in MIPv6: Modeling and Validation (MCK, KG), pp. 205–214.

SEFM-2007-AichernigPWW #consistency #formal method #industrial #protocol #testing

Protocol Conformance Testing a SIP Registrar: an Industrial Application of Formal Methods (BKA, BP, MW, FW), pp. 215–226.

SEFM-2007-MerayoN #consistency #probability #testing

Testing conformance on Stochastic Stream X-Machines (MGM, MN), pp. 227–236.

SEFM-2007-KahsaiRS #refinement #testing

Specification-based testing for refinement (TK, MR, BHS), pp. 237–246.

SEFM-2007-RungtaM #benchmark #metric #model checking

Hardness for Explicit State Software Model Checking Benchmarks (NR, EGM), pp. 247–256.

SEFM-2007-PernaG #model checking #specification

Model Checking RAISE Applicative Specifications (JIP, CG), pp. 257–268.

SEFM-2007-Cook #automation #concurrent #proving #source code

Automatically Proving Concurrent Programs Correct (BC), pp. 269–272.

SEFM-2007-DengRH #algorithm #execution #object-oriented #source code #symbolic computation #towards

Towards A Case-Optimal Symbolic Execution Algorithm for Analyzing Strong Properties of Object-Oriented Programs (XD, R, JH), pp. 273–282.

SEFM-2007-MehraRSJ #relational #verification

Verification of Object Relational Maps (KKM, SKR, APS, SKJ), pp. 283–292.

SEFM-2007-Lano #diagrams #interactive #specification #using

Formal Specification using Interaction Diagrams (KL), pp. 293–304.

SEFM-2007-LaneseMVR #distributed

Disciplining Orchestration and Conversation in Service-Oriented Computing (IL, FM, VTV, AR), pp. 305–314.

SEFM-2007-ZhuHLB #algebra #approach #semantics #web #web service

Algebraic Approach to Linking the Semantics of Web Services (HZ, JH, JL, JPB), pp. 315–328.

SEFM-2007-CansellGM #verification

Formal verification of tamper-evident storage for e-voting (DC, JPG, DM), pp. 329–338.

SEFM-2007-ColvinG #algorithm #scalability #stack #verification

A Scalable Lock-Free Stack Algorithm and its Verification (RC, LG), pp. 339–348.

SEFM-2007-SalehD #approach #novel #security #verification

Verifying Security Properties of Cryptoprotocols: A Novel Approach (MS, MD), pp. 349–360.

SEFM-2007-FraserB #configuration management #proving #tool support

Configurable Proof Obligations in the Frog Toolkit (SF, RB), pp. 361–370.

SEFM-2007-ReevesS #refinement

Feature Refinement (SR, DS), pp. 371–380.

SEFM-2007-CamaraSC #adaptation #behaviour #composition #runtime #transaction

Run-time Composition and Adaptation of Mismatching Behavioural Transactions (JC, GS, CC), pp. 381–390.

SEFM-2007-Hameurlain #behaviour #component #flexibility #protocol #specification

Flexible Behavioural Compatibility and Substitutability for Component Protocols: A Formal Specification (NH), pp. 391–400.