Proceedings of the Second International Conference on Software Engineering and Formal Methods
SEFM, 2004.

@proceedings{SEFM-2004,
	address       = "Beijing, China",
	ee            = "http://www.computer.org/csdl/proceedings/sefm/2004/2222/00/index.html",
	isbn          = "0-7695-2222-X",
	publisher     = "{IEEE Computer Society}",
	title         = "{Proceedings of the Second International Conference on Software Engineering and Formal Methods}",
	year          = 2004,
}

Contents (43 items)

7 ×#verification
6 ×#using
5 ×#testing
4 ×#generative
4 ×#refinement
4 ×#specification
3 ×#analysis
3 ×#architecture
3 ×#design
3 ×#distributed

SEFM-2004-Misra #distributed #programming #web #web service

A Programming Model for the Orchestration of Web Services (JM), pp. 2–11.

SEFM-2004-PangPE #abstraction #parallel #process

Abstraction of Parallel Uniform Processes with Data (JP, JvdP, MVE), pp. 14–23.

SEFM-2004-RouffVHTR #behaviour #formal method #predict

Properties of a Formal Method for Prediction of Emergent Behaviors in Swarm-Based Systems (CR, AV, MGH, WT, JLR), pp. 24–33.

SEFM-2004-Yoshiura #specification

Finding the Causes of Unrealizability of Reactive System Formal Specifications (NY), pp. 34–43.

SEFM-2004-TangW #mobile #process #towards

Towards Mobile Processes in Unifying Theories (XT, JW), pp. 44–53.

SEFM-2004-Roy #finite #infinity #using #verification

Symbolic Verification of Infinite Systems using a Finite Union of DFAs (SR), pp. 56–66.

SEFM-2004-SchuleS #comparison #infinity #model checking #verification

Global vs. Local Model Checking: A Comparison of Verification Techniques for Infinite State Systems (TS, KS), pp. 67–76.

SEFM-2004-BeckertK #deduction #proving #reuse #verification

Proof Reuse for Deductive Program Verification (BB, VK), pp. 77–86.

SEFM-2004-SistlaWZ #using

Checking Extended CTL properties Using Guarded Quotient Structures (APS, XW, MZ), pp. 87–94.

SEFM-2004-BaumeisterKW #development

Property-Driven Development (HB, AK, MW), pp. 96–102.

SEFM-2004-WenD #design #requirements

From Requirements Change to Design Change: A Formal Path (LW, RGD), pp. 104–113.

SEFM-2004-LanotteMT #decidability #parametricity #probability #security

Decidability Results for Parametric Probabilistic Transition Systems with an Application to Security (RL, AMS, AT), pp. 114–121.

SEFM-2004-MoisanRR #behaviour #component #formal method #framework #towards

Towards Formalizing Behavioral Substitutability in Component Frameworks (SM, AR, JPR), pp. 122–131.

SEFM-2004-NaiyongJ #co-evolution #design #hardware #modelling #specification

Resource Models and Pre-Compiler Specification for Hardware/Software Co-Design Language (NJ, JH), pp. 132–141.

SEFM-2004-SandersB #modelling #peer-to-peer #uml

Modeling Peer-to-Peer Service Goals in UML (RTS, RB), pp. 144–153.

SEFM-2004-FlakeM #bound #ocl

Past- and Future-Oriented Time-Bounded Temporal Properties with OCL (SF, WM), pp. 154–163.

SEFM-2004-MengNB #algebra #on the #perspective #refinement #semantics #uml

On Semantics and Refinement of UML Statecharts: A Coalgebraic View (SM, ZN, LSB), pp. 164–173.

SEFM-2004-SchinzTMW #uml #verification

The Rhapsody UML Verification Environment (IS, TT, CM, BW), pp. 174–183.

SEFM-2004-Joseph

Care, Feeding and Growth of Software Systems (MJ), p. 186–?.

SEFM-2004-JohnsenO #communication #concurrent #distributed

An Asynchronous Communication Model for Distributed Concurrent Objects (EBJ, OO), pp. 188–197.

SEFM-2004-ArbabBBR #component #logic #modelling

Models and Temporal Logics for Timed Component Connectors (FA, CB, FSdB, JJMMR), pp. 198–207.

SEFM-2004-BidoitHKB #black box #object-oriented #specification

Glass-Box and Black-Box Views on Object-Oriented Specifications (MB, RH, AK, HB), pp. 208–217.

SEFM-2004-LeinoS #c# #exception #safety

Exception Safety for C# (KRML, WS), pp. 218–227.

SEFM-2004-BerghoferN #higher-order #random testing #testing

Random Testing in Isabelle/HOL (SB, TN), pp. 230–239.

SEFM-2004-ZhangXW #constraints #execution #generative #symbolic computation #testing #theorem proving #using

Path-Oriented Test Data Generation Using Symbolic Execution and Constraint Solving Techniques (JZ, CX, XW), pp. 242–250.

SEFM-2004-BertoliniFFO #analysis #automaton #generative #network #probability #testing #using

Test Case Generation Using Stochastic Automata Networks: Quantitative Analysis (CB, AGF, PF, FMO), pp. 251–260.

SEFM-2004-HamonMR #generative #model checking #performance #testing

Generating Efficient Test Sets with a Model Checker (GH, LMdM, JMR), pp. 261–270.

SEFM-2004-LiYW #distributed #multi #testing

Distributed Testing of Multi Input/Output Transition System (ZL, XY, JW), pp. 271–280.

SEFM-2004-HuBG #algorithm #generative #optimisation #validation

Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations (YH, CWB, BG), pp. 281–289.

SEFM-2004-KammullerS #heuristic #refinement

Heuristics for Refinement Relations (FK, JWS), pp. 292–299.

SEFM-2004-WuY #ambiguity #concurrent #refinement #towards

Towards Action Refinement for Concurrent Systems with Causal Ambiguity (JW, HY), pp. 300–309.

SEFM-2004-OliveiraXC #refinement

Refine and Gabriel: Support for Refinement and Tactics (MO, MX, AC), pp. 310–319.

SEFM-2004-Struth #automation #reasoning #set

Automated Element-Wise Reasoning with Sets (GS), pp. 320–329.

SEFM-2004-NguyenM #analysis #consistency

A Formalism for Conformance Analysis and Its Applications (TNN, EVM), pp. 330–339.

SEFM-2004-Mei #architecture #lifecycle #named

ABC: Supporting Software Architectures in the Whole Lifecycle (HM), pp. 342–343.

SEFM-2004-LaibinisT #architecture #fault tolerance #specification

Fault Tolerance in a Layered Architecture: A General Specification Pattern in B (LL, ET), pp. 346–355.

SEFM-2004-KhedriB #architecture #design #functional

Formal Derivation of Functional Architectural Design (RK, IB), pp. 356–265.

SEFM-2004-HeJ #transaction #verification

Verification of the WAP Transaction Layer (YTH, RJ), pp. 366–375.

SEFM-2004-GeguangXSZHY #approach #clustering #hardware #multi

An Approach to Hardware/Software Partitioning for Multiple Hardware Devices Model (GP, XZ, SW, ZQ, JH, WY), pp. 376–385.

SEFM-2004-Sinnott #development #realtime #tool support

The Formal, Tool Supported Development of Real Time Systems (ROS), pp. 388–395.

SEFM-2004-Fronk #algebra #analysis #approach #automation #petri net #using

Using Relation Algebra for the Analysis of Petri Nets in a CASE Tool Based Approach (AF), pp. 396–405.

SEFM-2004-KazhamiakinPR #case study #requirements #using #verification #web #web service

Formal Verification of Requirements using SPIN: A Case Study on Web Services (RK, MP, MR), pp. 406–415.

SEFM-2004-EvansTLF #how #information management #verification

How to Verify Dynamic Properties of Information Systems (NE, HT, RL, MF), pp. 416–425.