Programs

8:00- 8:45

Registration

8:45- 9:00

Opening Session

9:00- 10:00

Keynote Speech
(Chair: Xuandong Li)
Perspectives in Probabilistic Verification
Joost-Pieter Katoen

10:00- 10:30

Coffee Break

10:30- 12:30

Model Checking
(Chair：Jianhua Zhao)

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

Bounded Model Checking of Compositional Processes.
Jun Sun, Yang Liu, Jinsong Dong and Jing Sun

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

Symbolic Model Checking APSL
Wanwei Liu, Ji Wang and Huowang Chen

12:30- 14:00

Lunch

14:00- 16:00

Program Analysis and Type Theory
(Chair: Haifeng Guo)

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

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

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

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

16:00- 16:30

Coffee Break

16:30- 18:30

Software Architecture, Framework and Process
(Chair: A.S.M Sajeev)

A Petri Net-based Approach for Supporting Aspect-oriented Modeling.
Lianwei Guan, Hao Hu and Jian Lu

A Model-Driven Method for the Development of Web Applications User Interaction Layer.
Ricardo Souza and Roberto Barros

A Conceptual Framework to Integrate Fault Prediction Sub-process for Software Product Lines
Cagatay Catal and Banu Diri

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

16:30- 18:30

Short Paper 1
(Chair: Bixin Li)

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

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

A Bigraphical Model for Web Services Composition
Min Zhang, Ling Shi, Longfei Zhu, Yifei Wang and Geguang Pu

Producing UML Models from Focal Specifications An Application to Airport Security Regulations
David Delahaye, Jean-Frédéric Etienne and Véronique Viguié Donzeau-Gouge

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

Effective Predicate Abstraction for Program Verification
Li Li, Ming Gu, Xiaoyu Song and Jianmin Wang

8:30- 9:30

Keynote Speech
(Chair: Jim Davies)
A Logical Framework for Software Testing
Wei Li

9:30- 10:00

Coffee Break

10:00- 12:30

Service-oriented Computing
(Chair: Jun Pang)

Reasoning about Channel Passing in Choreography.
Hongli Yang, Chao Cai, Liyang Peng, Xiangpeng Zhao and Zongyan Qiu

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

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

Modeling and Refining the Service-Oriented Requirement.
Xiaoxia Cao, Huaikou Miao and Qingguo XU

Transformation of BPEL Processes to Petri Nets.
Haiqiang Dun and Lifu Wang

12:30- 14:00

Lunch

14:00- 16:00

Verification and Validation
(Chair: Jianhua Zhao)

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

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

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

Specifying properties for Modular p-calculus.
Takashi Kitamura and Huimin Lin

16:00- 16:30

Coffee Break

16:30- 17:30

Software Testing
(Chair: Kaile Su)

Towards Automatically Generating Test Paths for Web Application Testing.
Huaikou Miao, Zhongsheng Qian and Bo Song

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

16:30- 17:30

Short Paper 2
(Chair: Xiaoying Bai)

Implementing Higher-order Control in Java
Gang Yu

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

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

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

8:30- 10:30

Logic Systems and Programming
(Chair：Huaikou Miao)

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

A Memoized Strategy for Preference Logic Programs.
Haifeng Guo

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

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

10:30- 11:00

Coffee Break

11:00- 12:00

Specification and Requirements
(Chair: David Delahaye)

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

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

12:00- 12:15

Closing Session

12:15- 13:30

Lunch

13:30- 18:00

Sightseeing