2. TASE 2008: Nanjing, China

Keynote Speech

• Joost-Pieter Katoen:
  Perspectives in Probabilistic Verification. 3-10
  
• Wei Li:
  A Logical Framework for Software Testing. 11
  

Model Checking

• Corinna Spermann, Michael Leuschel:
  ProB gets Nauty: Effective Symmetry Reduction for B and Z Models. 15-22
  
• Jun Sun, Yang Liu, Jin Song Dong, Jing Sun:
  Bounded Model Checking of Compositional Processes. 23-30
  
• Jinji Yang, Kaile Su, Qingliang Chen:
  Improving Encoding Efficiency for Bounded Model Checking. 31-38
  
• Wanwei Liu, Ji Wang, Huowang Chen, Xiaodong Ma:
  Symbolic Model Checking APSL. 39-46
  

Program Analysis and Type Theory

• Zhifang Wang, Yiyun Chen, Zhenming Wang, Wei Wang, Bo Tian:
  An Extension to Pointer Logic for Verification. 49-56
  
• Shuling Wang, Zongyan Qiu:
  A Generic Model for Confinement and its Application. 57-64
  
• Yang Zhao, John Boyland:
  A Fundamental Permission Interpretation for Ownership Types. 65-72
  
• Ganesh M. Narayan, K. Gopinath, Sridhar Varadarajan:
  Structure and Interpretation of Computer Programs. 73-80
  

Software Architecture, Framework, and Process

• Lianwei Guan, Xingyu Li, Hao Hu:
  A Petri Net-Based Approach for Supporting Aspect-Oriented Modeling. 83-90
  
• Ricardo A. C. de Souza, Roberto Souto Maior de Barros:
  A Model-Driven Method for the Development of Web Applications User Interaction Layer. 91-98
  
• Cagatay Catal, Banu Diri:
  A Conceptual Framework to Integrate Fault Prediction Sub-Process for Software Product Lines. 99-106
  

Short Paper 1

• Christoph Knieke, Michaela Huhn, Malte Lochau:
  Executable Requirements Specification: Formal Semantics of Live Activity Diagrams. 109-112
  
• Tian Zhang, Frédéric Jouault, Jean Bézivin, Jianhua Zhao:
  A MDE Based Approach for Bridging Formal Models. 113-116
  
• Min Zhang, Ling Shi, Longfei Zhu, Yifei Wang, Libo Feng, Geguang Pu:
  A Bigraphical Model of WSBPEL. 117-120
  
• David Delahaye, Jean-Frédéric Étienne, Véronique Donzeau-Gouge:
  Producing UML Models from Focal Specifications: An Application to Airport Security Regulations. 121-124
  
• Soodeh Hosseini, Mohammad Abdollahi Azgomi:
  UML Model Refactoring with Emphasis on Behavior Preservation. 125-128
  
• Li Li, Ming Gu, Xiaoyu Song, Jianmin Wang:
  Effective Predicate Abstraction for Program Verification. 129-132
  

Service-Oriented Computing

• Hongli Yang, Chao Cai, Liyang Peng, Xiangpeng Zhao, Zongyan Qiu:
  Reasoning about Channel Passing in Choreography. 135-142
  
• Antonio Brogi, Razvan Popescu:
  Workflow Semantics of Peer and Service Behaviour. 143-150
  
• Chenguang Luo, Shengchao Qin, Zongyan Qiu:
  Verifying BPEL-Like Programs with Hoare Logic. 151-158
  
• Xiaoxia Cao, Huaikou Miao, Qingguo Xu:
  Modeling and Refining the Service-Oriented Requirement. 159-165
  
• Haiqiang Dun, Haiying Xu, Lifu Wang:
  Transformation of BPEL Processes to Petri Nets. 166-173
  

Verification and Validation

• Taolue Chen, Tingting Han, Joost-Pieter Katoen:
  Time-Abstracting Bisimulation for Probabilistic Timed Automata. 177-184
  
• Jun Pang, Zhengqin Luo, Yuxin Deng:
  On Automatic Verification of Self-Stabilizing Population Protocols. 185-192
  
• Taolue Chen, Jaco van de Pol, Yanjing Wang:
  PDL over Accelerated Labeled Transition Systems. 193-200
  
• Takashi Kitamura, Huimin Lin:
  Specifying Properties for Modular Pi-Calculus. 201-208
  

Software Testing

• Huaikou Miao, Zhong-sheng Qian, Bo Song:
  Towards Automatically Generating Test Paths for Web Application Testing. 211-218
  
• Hui Ruan, Jian Zhang, Jun Yan:
  Test Data Generation for C Programs with String-Handling Functions. 219-226
  

Short Paper 2

• Gang Yu:
  Implementing Higher-Order Control in Java. 229-232
  
• Haihao Shen, Sai Zhang, Jianjun Zhao:
  An Empirical Study of Maintainability in Aspect-Oriented System Evolution Using Coupling Metrics. 233-236
  
• Sakgasit Ramingwong, A. S. M. Sajeev:
  A Multidimensional Model for Mum Effect in Offshore Outsourcing. 237-240
  
• Lian Yu, Shuang Su, Shan Luo, Yu Su:
  Completeness and Consistency Analysis on Requirements of Distributed Event-Driven Systems. 241-244
  

Logic Systems and Programming

• Liannan Lin, Jinzhao Wu, Xiang Xu:
  Open Logic Based on Partial-Ordered Partition Model. 247-254
  
• Hai-Feng Guo:
  A Memoized Strategy for Preference Logic Programs. 255-262
  
• Shuling Wang, Luís Soares Barbosa, José Nuno Oliveira:
  A Relational Model for Confined Separation Logic. 263-270
  
• Zhenhua Duan, Nan Zhang:
  A Complete Axiomatization of Propositional Projection Temporal Logic. 271-278
  

Specification and Requirements

• Zheng Fu, Graeme Smith:
  Towards More Flexible Development of Z Specifications. 281-288
  
• Lan Lin, Jesse H. Poore:
  Pushing Requirements Changes through to Changes in Specifications. 289-296
  
• Arnaud Lanoix:
  Event-B Specification of a Situated Multi-Agent System: Study of a Platoon of Vehicles. 297-304