You should prepare your slides in pdf or ppt file before the presentations.
|
Tuesday, 31 October 2006
|
|
19:30
|
RECEPTION AT UNU-IIST
|
| *********** |
|
|
Wednesday, 1 November 2006
|
|
0830 - 0900
|
Registration
|
|
0900 - 0930
|
Openning Session (Chair: Chris George)
|
|
0930 - 1030
|
Zhou Chaochen, Keynote Talk 1 (Chair: Dines Bijoner)
Title: Program Verification through Computer Algebra
|
|
1030 - 1100
|
Break
|
|
1100 - 1230
|
Session A
|
1: Specification and Verification (Chair: John Derric)
|
|
Paper ID:
Paper title:
Paper authors:
|
53
A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces
Bernhard Beckert, Gerd Beuster
|
|
Paper ID:
Paper title:
Paper authors:
|
74
Applying Timed Interval Calculus to Simulink Diagrams
Chunqing Chen, Jin Song Dong
|
|
Paper ID:
Paper title:
Paper authors:
|
92
Reducing Model Checking of the Few to the One
E. Allen Emerson, Richard J. Trefler, Thomas Wahl
|
|
|
Session B
|
1: Internetware (Chair: He Jifeng)
|
|
Paper ID:
Paper title:
Paper authors:
|
55
Context Ontology-based Capability Specification for Web Service Discovery
Puwei Wang, Zhi Jin, Lin Liu
|
|
Paper ID:
Paper title:
Paper authors:
|
111
User-defined Atomicity Constraint: A More Flexible Transaction Model for Reliable Service Composition
Xiaoning Ding, Jun Wei, Tao Huang
|
|
Paper ID:
Paper title:
Paper authors:
|
113
Scenario-based Component Behavior Derivation
Yan Zhang, Jun Hu, Xiaofeng Yu, Tian Zhang, Xuandong Li, Guoliang Zheng
|
|
|
1230 - 1430
|
Lunch
|
|
1430 - 1600
|
Session A
|
2: Verification (Chair: Abhik Roychoudhury)
|
|
Paper ID:
Paper title:
Paper authors:
|
59
Induction-Guided Falsification
Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi
|
|
Paper ID:
Paper title:
Paper authors:
|
31
Verifying Chi Models of Industrial Systems with SPIN
Nikola Trcka
|
|
Paper ID:
Paper title:
Paper authors:
|
83
Stateful Dynamic Partial-Order Reduction
Xiaodong Yi, Ji Wang, Xuejun Yang
|
|
|
Session B
|
2: Web-Based Systems (Chair: Antonio Cerone)
|
|
Paper ID:
Paper title:
Paper authors:
|
48
Verification of Computation Orchestration via Timed Automata
Jin Song Dong, Yang Liu, Jun Sun, Xian Zhang
|
|
Paper ID:
Paper title:
Paper authors:
|
70
Towards the Semantics for Web Service Choreography Description Language
Jing Li, Jifeng He, Geguang Pu, Huibiao Zhu
|
|
Paper ID:
Paper title:
Paper authors:
|
107
Type Checking Choreography Description Language
Hongli Yang , Xiangpeng Zhao, Zongyan Qiu, Chao Cai, Geguang Pu
|
|
|
1600 - 1630
|
Break
|
|
1630 - 1800
|
Session A
|
3: Concurrency and Communication (Chair: Gary T. Leavens)
|
|
Paper ID:
Paper title:
Paper authors:
|
12
Formalising progress properties of non-blocking programs
Brijesh Dongol
|
|
Paper ID:
Paper title:
Paper authors:
|
49
Towards a fully generic theory of data
Douglas A. Creager, Andrew C. Simpson
|
|
Paper ID:
Paper title:
Paper authors:
|
47
Verifying Statemate Statechartss Using CSP and FDR
Bill Roscoe, Zhenzhong Wu
|
|
|
Session B
|
3: Modelling and Reasoning (Chair: Martin Leucker)
|
|
Paper ID:
Paper title:
Paper authors:
|
32
A Reasoning Method for Time CSP based on Constraint Solving
Jin Song Dong, Ping Hao, Jun Sun, Xian Zhang
|
|
Paper ID:
Paper title:
Paper authors:
|
37
Mapping RT-LOTOS specifications into Time Petri Nets
Tarek Sadani, Marc Boyer, Pierre de Saqui-Sannes, Jean-Pierre Courtiat
|
|
Paper ID:
Paper title:
Paper authors:
|
42
Reasoning Algebraically about Probabilistic Loops
Larissa Meinicke, Ian J. Hayes
|
|
|
1930
|
Dinner
|
|
***********
|
|
Thursday 2 November
|
|
0930 - 1030
|
Gary T. Leavens, FME Keynote Talk 2 (Chair: Mike Reed)
Title: JML's Rich, Inherited Specifications for Behavioral Subtypes
|
|
1030 - 1100
|
Break
|
|
1100 - 1230
|
Session A
|
4: Object and Component Orientation (Chair: Heike Wehrheim)
|
|
Paper ID:
Paper title:
Paper authors:
|
17
Formal Verification of the Heap Manager of an Operating System using Separation Logic
Nicolas Marti, Reynald Affeldt, Akinori Yonezawa
|
|
Paper ID:
Paper title:
Paper authors:
|
98
A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs
Bart Jacobs, Jan Smans, Frank Piessens, Wolfram Schulte
|
|
Paper ID:
Paper title:
Paper authors:
|
68
Model Checking Dynamic UML Consistency
Xiangpeng Zhao, Quan Long, Zongyan Qiu
|
|
|
Session B
|
4: Testing (Chair: Bernhard Aichernig)
|
|
Paper ID:
Paper title:
Paper authors:
|
46
Conditions for Avoiding Controllability Problems in Distributed Testing
Jessica Chen, Lihua Duan
|
|
Paper ID:
Paper title:
Paper authors:
|
65
Generating Test Cases for Constraint Automata by Genetic Symbiosis Algorithm
Samira Tasharofi, Sepand Ansari, Marjan Sirjani
|
|
Paper ID:
Paper title:
Paper authors:
|
18
Checking the Conformance of Java Classes Against Algebraic Specifications
Isabel Nunes, Antónia Lopes, Vasco Vasconcelos, João Abreu, Luis S. Reis
|
|
|
1230 - 1430
|
Lunch
|
|
1430 - 1600
|
Session A
|
5: Tools (Chair: Natarajan Shankar)
|
|
Paper ID:
Paper title:
Paper authors:
|
62
A Tool for a Formal Pattern Modeling Language
Soon-Kyeong Kim , David Carrington
|
|
Paper ID:
Paper title:
Paper authors:
|
95
An open extensible tool environment for Event-B
Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede
|
|
Paper ID:
Paper title:
Paper authors:
|
103
Tool for translating Simulink models into input language of a
Meenakshi Balasubramanian, Abhishek Bhatnagar, Sudeepa Roy
|
|
|
Session B
|
5: Fault-Tolerance and Security (Chair: Keijiro Araki)
|
|
Paper ID:
Paper title:
Paper authors:
|
61
Verifying Abstract Information Flow Properties in Fault Tolerant Security Devices
Tim McComb, Luke Wildman
|
|
Paper ID:
Paper title:
Paper authors:
|
63
A Language for Modeling Network Availability
Luigia Petre, Kaisa Sere, Marina Walden
|
|
Paper ID:
Paper title:
Paper authors:
|
91
Multi-Process Systems Analysis using Event B: Application to Group Communication Systems
Christian Attiogbé
|
|
|
1600 - 1630
|
Break
|
|
1630 - 1800
|
Session A
|
6: Abstraction and Refinement (Chair: Shaoying Liu)
|
|
Paper ID:
Paper title:
Paper authors:
|
34
Issues in implementing a model checker for Z
John Derrick, Siobhan North, Tony Simons
|
|
Paper ID:
Paper title:
Paper authors:
|
38
Taking our own medicine: applying the refinement calculus to state-rich refinement model checking
Leo Freitas, Ana Cavalcanti, Jim Woodcock
|
|
Paper ID:
Paper title:
Paper authors:
|
50
Discovering Likely Method Specifications
Nikolai Tillmann, Feng Chen, Wolfram Schulte
|
|
|
Session B
|
6: Model Checking (Chair: Wang Ji)
|
|
Paper ID:
Paper title:
Paper authors:
|
16
Incremental Slicing
Heike Wehrheim
|
|
Paper ID:
Paper title:
Paper authors:
|
90
Assume-Guarantee Software Verification Based on Game Semantics
Aleksandar Dimovski, Ranko Lazic
|
|
Paper ID:
Paper title:
Paper authors:
|
96
Optimized Execution of Deterministic Blocks in Java PathFinder
Marcelo d`Amorim, Ahmed Sobeih, Darko Marinov
|
|
|
1930
|
Conference Banquet
|
|
***********
|
|
Friday 3 November
|
|
0930 - 1030
|
John McDermid, Keynote Talk 3 (Chair: Chris George)
Title: Three Perspectives in Formal Engineering
|
|
1030 - 1100
|
Break
|
|
1100 - 1200
|
Session Specification and Design (Chair: Paul Curzon)
|
|
Paper ID:
Paper title:
Paper authors:
|
60
Time Aware Modelling and Analysis of Multiclocked VLSI Systems
Tomi Westerlund, Juha Plosila
|
|
Paper ID:
Paper title:
Paper authors:
|
28
SALT---Structured Assertion Language for Temporal Logic
Andreas Bauer, Martin Leucker, Jonathan Streit
|
|
|
1200 - 1230
|
Closing Session (Chair: Zhiming Liu) |
|
1230 - 1400
|
Lunch
|