August 24, 2010 (Tuesday) |
| 1000 - 1200 |
Tutorial I : Professor Jean-Raymond Abrial. |
|
Modeling, Refining, and Proving with Event-B
(Methodology of Software Development) |
|
slides
report
biography
cv
|
| 1200 - 1400 |
Lunch |
| 1400 - 1600 |
Tutorial II : Professor Yih-Kuen Tsay. |
|
Assume-Guarantee Reasoning |
|
abstract |
| 1800 - 2000 |
Reception |
August 25, 2010 (Wednesday) |
| 0830 - 0900 |
Openning session |
| 0900 - 1000 |
Session I |
|
Invited talk : Prof. Jean-Raymond Abrial |
|
Constructing a Prover Devoted to Set Theoretic Proofs |
|
abstract
report
biography
cv
|
|
Chair: Yih-Kuen Tsay |
| 1000 - 1030 |
Coffee break |
| 1030 - 1200 |
Session II: Formal Models |
|
Chair: Churn-Jung Liau |
|
Yongxin Zhao, Zheng Wang, Geguang Pu and Huibiao Zhu.
A Formal Model for Service Choreography with Exception Handling and Finalization |
|
Chen-Wei Wang, Jim Davies and James Welch.
A Guarded Workflow Language and its Formal Semantics |
|
Hung Ledang and Hubert Dubois.
Proving Model Transformations |
| 1200 - 1400 |
lunch |
| 1400 - 1530 |
Session III: Program Verification |
|
Chair: Jonanthan Lee |
|
Zhaopeng Li, Zhong Zhuang, Yiyun Chen, Simin Yang, Zhenting Zhang and Dawei Fan.
A Certifying Compiler for Clike Subset of C Language |
|
Shengyi Wang, Zongyan Qiu, Shengchao Qin and Wei-Ngan Chin.
Stack Bound Inference for Abstract Java Bytecode |
|
Liu Pan, Miao Huaikou and Mei Jia.
Efficient Algorithms for Building the Sets P and W |
| 1530 - 1600 |
Coffee break |
| 1630 - 1800 |
Session IV: Logics |
|
Chair: Yu-Fang Chen |
|
Lin Zhao, Tao Tang, Jinzhao Wu and Tianhua Xu.
Runtime Verification with Multi-Valued Formula Rewriting |
|
Xiaoxiao Yang.
Axiomatic Interval Temporal Logic Verification |
|
Hong Zhu.
On the Theoretical Foundation of Meta-Modelling in Graphically Extended BNF and First Order Logic |
| 1830 - 2200 |
Social Event |
August 26, 2010 (Thursday) |
| 0900 - 1000 |
Session V |
|
Invited talk : Saddek Bensalem (VERIMAG) |
|
Component-Based Design of Real-Time Systems in BIP |
|
Chair: Farn Wang |
| 1000 - 1030 |
Coffee break |
| 1030 - 1200 |
Session VI: Model-Checking |
|
Chair: Doron A. Peled |
|
Kahloul Laid, Chaoui Allaoua and Djouani Karim.
Modeling Reconfirgurable Systems Using Flexible Petri Nets |
|
Yunhe Wang, Bo Jiang and Li Jiao.
Property Checking for 1-Place-Unbounded Petri Nets |
|
Haibin Zhang and Zhenhua Duan.
Model Checking Rectangular Hybrid Systems With Timed Computation Tree Logic |
| 1200 - 1400 |
Lunch |
| 1400 - 1500 |
Session VII: Process Algebrae |
|
Chair: Hsu-Chun Yen |
|
Zining Cao.
Bisimulations for Open Processes in Higher Order Pi-Calculus |
|
Moritz Kleine and Thomas Gothel.
Specification, Verification and Implementation of Business Processes using CSP |
| 1500 - 1530 |
Coffee break |
| 1530 - 1630 |
Session VIII: Synthesis |
|
Chair: Jean-Raymond Abrial |
|
Saddek Bensalem, Axel Legay, Thanh Hung Nguyen, Joseph Sifakis and Rongjie Yan.
Incremental Invariant Generation for Compositional Design |
|
Fei He, He Zhu, William N. N. Hung, Xiaoyu Song and Ming Gu.
Compositional Abstraction Refinement for Timed Systems |
| 1630 - 1700 |
Coffee break |
| 1700 - 1800 |
Session IX: Poster Papers |
|
Chair: Saddek Bensalem |
|
Hai Wan, Xiaoyu Song and Ming Gu.
Parameterized Specifying and Verifying PLC Systems in Coq |
|
Farn Wang.
Lazy Decision Diagrams for Word-Level Model Manipulation in Software Verification |
|
Raghava Rao Mukkamala and Thomas Hildebrandt.
From Dynamic Condition Response Structures to Buechi Automata |
| 1830 - 2100 |
PC Meeting |
August 27, 2010 (Friday) |
| 0900 - 1000 |
Session X |
|
Invited talk : Libra C.Y. Huang (IBM, Taiwan) |
|
Building a Smarter Planet with Smarter Products |
|
Chair: Jing Liu |
| 1000 - 1030 |
Coffee break |
| 1030 - 1200 |
Session XI: Complex Systems |
|
Chair: Fang Yu |
|
Yongxin Zhao, Yanhong Huang, Jianwen Li and Huibiao Zhu.
Probabilistic Model of System Survivability |
|
Jianjun Xu, Qingping Tan and Wanwei Liu.
Estimating the Soft Error Vulnerability of Register Files via Interprocedural Data Flow Analysis |
|
Shengbo Chen.
Towards Practical Modeling of Web Applications and Generating Tests |
| 1200 - 1800 |
Lunch and excursion |
| 1800 - 2100 |
Banquet |
|
|
