2. SEFM 2004: Beijing, China

Keynote 1

• Jayadev Misra:
  A Programming Model for the Orchestration of Web Services. 2-11
  

Session 1A: Parallel Distributed Systems

• Jun Pang, Jaco van de Pol, Miguel Valero Espada:
  Abstraction of Parallel Uniform Processes with Data. 14-23
  
• Christopher Rouff, Amy Vanderbilt, Michael G. Hinchey, Walt Truszkowski, James L. Rash:
  Properties of a Formal Method for Prediction of Emergent Behaviors in Swarm-Based Systems. 24-33
  
• Noriaki Yoshiura:
  Finding the Causes of Unrealizability of Reactive System Formal Specifications. 34-43
  
• Xinbei Tang, Jim Woodcock:
  Towards Mobile Processes in Unifying Theories. 44-53
  

Session 1B: Automated Proof and Model Checking

• Suman Roy:
  Symbolic Verification of Infinite Systems using a Finite Union of DFAs. 56-66
  
• Tobias Schüle, Klaus Schneider:
  Global vs. Local Model Checking: A Comparison of Verification Techniques for Infinite State Systems. 67-76
  
• Bernhard Beckert, Vladimir Klebanov:
  Proof Reuse for Deductive Program Verification. 77-86
  
• A. Prasad Sistla, Xiaodong Wang, Min Zhou:
  Checking Extended CTL properties Using Guarded Quotient Structures. 87-94
  

Keynote 2

• Hubert Baumeister, Alexander Knapp, Martin Wirsing:
  Property-Driven Development. 96-102
  

Session 2A: System Modelling and Development

• Lian Wen, R. Geoff Dromey:
  From Requirements Change to Design Change: A Formal Path. 104-113
  
• Ruggero Lanotte, Andrea Maggiolo-Schettini, Angelo Troina:
  Decidability Results for Parametric Probabilistic Transition Systems with an Application to Security. 114-121
  
• Sabine Moisan, Annie Ressouche, Jean-Paul Rigault:
  Towards Formalizing Behavioral Substitutability in Component Frameworks. 122-131
  
• Naiyong Jin, Jifeng He:
  Resource Models and Pre-Compiler Specification for Hardware/Software Co-Design Language. 132-141
  

Session 2B: Model Integration and Theory Unification

• Richard Torbjørn Sanders, Rolv Bræk:
  Modeling Peer-to-Peer Service Goals in UML. 144-153
  
• Stephan Flake, Wolfgang Müller:
  Past- and Future-Oriented Time-Bounded Temporal Properties with OCL. 154-163
  
• Sun Meng, Zhang Naixiao, Luís Soares Barbosa:
  On Semantics and Refinement of UML Statecharts: A Coalgebraic View. 164-173
  
• Ingo Schinz, Tobe Toben, Christian Mrugalla, Bernd Westphal:
  The Rhapsody UML Verification Environment. 174-183
  

Keynote 3

• Mathai Joseph:
  Care, Feeding and Growth of Software Systems. 186-
  

Session 3: Object-Oriented and Component-Based Development

• Einar Broch Johnsen, Olaf Owe:
  An Asynchronous Communication Model for Distributed Concurrent Objects. 188-197
  
• Farhad Arbab, Christel Baier, Frank S. de Boer, Jan J. M. M. Rutten:
  Models and Temporal Logics for Timed Component Connectors. 198-207
  
• Michel Bidoit, Rolf Hennicker, Alexander Knapp, Hubert Baumeister:
  Glass-Box and Black-Box Views on Object-Oriented Specifications. 208-217
  
• K. Rustan M. Leino, Wolfram Schulte:
  Exception Safety for C#. 218-227
  

Keynote 4

• Stefan Berghofer, Tobias Nipkow:
  Random Testing in Isabelle/HOL. 230-239
  

Session 4A: Testing and Validation

• Jian Zhang, Chen Xu, Xiaoliang Wang:
  Path-Oriented Test Data Generation Using Symbolic Execution and Constraint Solving Techniques. 242-250
  
• Cristiano Bertolini, André G. Farina, Paulo Fernandes, Flávio Moreira Oliveira:
  Test Case Generation Using Stochastic Automata Networks: Quantitative Analysis. 251-260
  
• Grégoire Hamon, Leonardo Mendonça de Moura, John M. Rushby:
  Generating Efficient Test Sets with a Model Checker. 261-270
  
• Zhongjie Li, Xia Yin, Jianping Wu:
  Distributed Testing of Multi Input/Output Transition System. 271-280
  
• Ying Hu, Clark W. Barrett, Benjamin Goldberg:
  Theory and Algorithms for the Generation and Validation of Speculative Loop Optimizations. 281-289
  

Session 4B: System Correctness Analysis and Refinement

• Florian Kammüller, Jeff W. Sanders:
  Heuristics for Refinement Relations. 292-299
  
• Jinzhao Wu, Houguang Yue:
  Towards Action Refinement for Concurrent Systems with Causal Ambiguity. 300-309
  
• Marcel Oliveira, Manuela Xavier, Ana Cavalcanti:
  Refine and Gabriel: Support for Refinement and Tactics. 310-319
  
• Georg Struth:
  Automated Element-Wise Reasoning with Sets. 320-329
  
• Tien Nhut Nguyen, Ethan V. Munson:
  A Formalism for Conformance Analysis and Its Applications. 330-339
  

Keynote 5

• Hong Mei:
  ABC: Supporting Software Architectures in the Whole Lifecycle. 342-343
  

Session 5A: Architecture and Co-Design

• Linas Laibinis, Elena Troubitsyna:
  Fault Tolerance in a Layered Architecture: A General Specification Pattern in B. 346-355
  
• Ridha Khédri, Imen Bourguiba:
  Formal Derivation of Functional Architectural Design. 356-265
  
• Yu-Tong He, Ryszard Janicki:
  Verification of the WAP Transaction Layer. 366-375
  
• Geguang Pu, Xiangpeng Zhao, Shuling Wang, Zongyan Qiu, Jifeng He, Wang Yi:
  An Approach to Hardware/Software Partitioning for Multiple Hardware Devices Model. 376-385
  

Session 5B: Automated Analysis and Verification

• Richard O. Sinnott:
  The Formal, Tool Supported Development of Real Time Systems. 388-395
  
• Alexander Fronk:
  Using Relation Algebra for the Analysis of Petri Nets in a CASE Tool Based Approach. 396-405
  
• Raman Kazhamiakin, Marco Pistore, Marco Roveri:
  Formal Verification of Requirements using SPIN: A Case Study on Web Services. 406-415
  
• Neil Evans, Helen Treharne, Régine Laleau, Marc Frappier:
  How to Verify Dynamic Properties of Information Systems. 416-425