default search action
2nd SEFM 2004: Beijing, China
- 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 28-30 September 2004, Beijing, China. IEEE Computer Society 2004, ISBN 0-7695-2222-X
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 A. 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
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.
last updated on 2024-12-19 22:18 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: