Accetped Papers

Accepted as full papers, total 30

1. Zhenhua Duan and Nan Zhang. A Complete Axiomatization of Propositional Projection Temporal Logic.

2. Jun Sun, yang liu, jin song dong and Jing Sun. Bounded Model Checking of Compositional Processes.

3. Huaikou Miao, QIAN Zhong-sheng and Bo Song. Towards Automatically Generating Test Paths for Web Application Testing.

4. Chenguang Luo, Shengchao Qin and Zongyan Qiu. Verifying BPEL-like Programs with Hoare Logic.

5. CAO Xiao-Xia, Huaikou Miao and Qingguo XU.Modeling and Refining the Service-Oriented Requirement.

6. Jun Pang, Zhengqin Luo and Yuxin Deng. On Automatic Verification of Self-stabilizing Population Protocols.

7. Zheng Fu and Graeme Smith. Towards More Flexible Development of Z Specifications.

8. Taolue Chen, Jaco van de Pol and Yanjing Wang. Model Checking and Axiomatization for PDL on Accelerated Labelled Transition Systems.

9. Shuling Wang and Zongyan Qiu. A Generic Model for Confinement and its Application.

10. Zhifang Wang, Yiyun Chen, Zhenming Wang, Wei Wang and Bo Tian. An Extension to Pointer Logic for Verification.

11. Shuling Wang, Luis Barbosa and Jose Oliveira. A Relational Model for Confined Separation Logic.

12. hongli yang, Chao Cai, Liyang Peng, Xiangpeng Zhao and Zongyan Qiu. Reasoning about Channel Passing in Choreography.

13. Liannan Lin, Jinzhao Wu and Xiang Xu. Open Logic Based on Partial-Ordered Partition Model.

14. Lianwei Guan, Xingyu Li, Hao Hu. A Petri Net-based Approach for Supporting Aspect-oriented Modeling.

15. Taolue Chen, Tingting Han and Joost-Pieter Katoen. Time-Abstracting Bisimulation for Probabilistic Timed Automata.

16. ricardo souza and Roberto Barros. A Model-Driven Method for the Development of Web Applications User Interaction Layer.

17. Corinna Spermann and Michael Leuschel. ProB gets Nauty: Effective Symmetry Reduction for B and Z models.

18. Augustin Kebemou and Ina Schieferdecker. AutomotiveArchitect: An Environment for the Design of Automotive Systems Architectures.

19. Takashi Kitamura and Huimin Lin. Specifying properties for Modular $\pi$-calculus.

20. Antonio Brogi and Razvan Popescu. Workflow Semantics of Peer and Service Behaviour.

21. HaiQiang Dun and LiFu Wang. Transformation of BPEL Processes to Petri Nets.

22. JinJi Yang, Kaile Su and Qingliang Chen. Improving Encoding Efficiency for Bounded Model Checking.

23. Hai-Feng Guo. A Memoized Strategy for Preference Logic Programs.

24. Hui Ruan, Jian Zhang and Jun Yan. Test data generation for C programs with string-handling functions.

25. Arnaud Lanoix. Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles.

26. Yang Zhao and John Boyland. A Fundamental Permission Interpretation for Ownership Types.

27. Ganesh Narayan, K. Gopinath and Sridhar Varadarajan. Structure and Interpretation of Computer Programs

28. Lan Lin and Jesse H. Poore. Pushing Requirements Changes through to Changes in Specifications

29. Cagatay Catal and banu diri. A Conceptual Framework to Integrate Fault Prediction Sub-process for Software Product Lines

30. Wanwei Liu, Ji Wang, Huowang Chen and Xiaodong Ma. Symbolic Model Checking APSL

Accepted as short papers:

1. Christoph Knieke, Michaela Huhn and Malte Lochau. Executable Requirements Specification: Formal Semantics of Live Activity Diagrams

2. Min ZHANG, Ling Shi, Longfei Zhu, Yifei Wang and Geguang Pu. A Bigraphical Model of WSBPEL

3. Lian Yu, Shuang Su, Shan Luo and Yu Su. Completeness and Consistency Analysis on Requirements of Distributed Event-Driven Systems

4. li l, Ming Gu, Xiaoyu Song and Wang Jianmin. Effective Predicate Abstraction for Program Verification

5. Tian Zhang, Frédéric Jouault, Jean Bezivin and Jianhua Zhao. A MDE Based Approach for Bridging Formal Models

6. David Delahaye, Jean-Frédéric ?tienne and Véronique Viguié Donzeau-Gouge. Producing UML Models from Focal Specifications: an Application to Airport Security Regulations

7. Haihao Shen, Sai Zhang and Jianjun Zhao. An Empirical Study of Maintainability in Aspect-Oriented System Evolution Using Coupling Metrics

8. Gang Yu. Implementing Higher-Order Control in Java

9. Sakgasit Ramingwong and A.S.M. Sajeev. A Multidimensional Model for Mum Effect in Offshore Outsourcing

10. Soodeh Hosseini and Mohammad Abdollahi Azgomi. Formal Specification of UML Model Refactoring with Emphasis on Behavior Preserving