TUESDAY, 21ST SEPTEMBER 2004
|
|
14:00 - 18:00
|
REGISTRATION
|
|
19:00 - 21:30
|
RECEPTION
|
WEDNESDAY, 22ND SEPTEMBER 2004
|
|
|
|
8:00 - 9:00
|
REGISTRATION
|
|
9:00 - 9:30
|
OPENING SEESION (Chair: Danning Li, Guizhou Academy of
Sciences, China)
|
|
|
Welcome Speech
Someone from the local organization
About UNU-IIST: Jifeng He,
UNU-IIST, Macao
Report on the Work of the Program
Committee
Zhiming Liu, PC Co-chair of ICTAC 2004, UNU-IIST, Macao
|
|
9:30 - 10:30
|
KEYNOTE TALK 1 (Chair: Keijiro Araki, Kyushu University,
Japan)
|
|
|
Jifeng He, UNU-IIST, Macao
|
|
10:30 - 11:00
|
BREAK
|
|
11:00 - 13:00
|
SESSION 1A: AUTOMATA THEORY AND LOGICS (Chair: Huimin Lin,
Institute of Software, Chinese Academy of Sciences, China)
|
|
|
Reasoning about co-Büchi Tree
Automata
Salvatore La Torre and Aniello Murano (Università degli Studi di Salerno,
Italy)
Switched Probabilistic I/O
Automata
Ling Cheung, Frits Vaandrager (University of Nijmegen, The Netherlands),
Nancy Lynch (MIT Computer Science and Artifical Intelligence Laboratory,
USA) and Roberto Segala (Università di Verona, Italy)
Foundations for the Run-time Monitoring of
Reactive Systems - Fundamentals of the MaC language
Mahesh Viswanathan (University of Illinois at Urbana Champaign, USA) and
Moonzoo Kim (Pohang University of Science and Technology,
Korea)
Duration Calculus: A Real-time Semantic for
B
Samuel Colin, Georges Mariano (INRETS, France) and Vincent Poirriez (LAMIH,
France)
|
|
11:00 - 13:00
|
SESSION 1B: REAL-TIME AND CO-DESIGN (Chair: Paddy Krishnan,
Bond University, Australia)
|
|
|
An Algebraic Approach for
Codesign
Marc Aiguier, Stefan Béroff (Université d'Évry Val d'Essonne, France) and
Pierre-Yves Schobbens (Institut d'Informatique, Belgium)
A Framework for Specification and
Validation of Real-time Systems using Circus Actions
Adnan Sherif, Augusto Sampaio (CIn/UFPE, Brazil), He Jifeng
(UNU-IIST, Macao) and Ana Cavalcante (University of Kent, UK)
A Calculus for Shapes in Time and
Space
Andreas Schäefer (University of Oldenburg, Germany)
An Algebra of Petri Nets with Arc-based
Time Restrictions
Apostolos Niaouris (University of Newcastle, UK)
|
|
13:00 - 14:30
|
LUNCH
|
|
14:30 - 15:30
|
KEYNOTE TALK 2 (Chair: K. Rustan M. Leino, Microsoft
Research, USA)
|
|
|
Jose Luiz Fiadeiro, University of Leicester, UK
|
|
15:30 - 16:00
|
BREAK
|
|
16:00 - 18:00
|
SECTION 2A: SYSTEM MODELLING AND APPLICATION OF LOGICS
(Chair: Raymond Boute, Ghent University, Belgium)
|
|
|
Atomic Components
Steve Reeves and David Streader (University of Waikato, New Zealand)
A Proof of Weak Termination Providing the
Right Way to Terminate
Olivier Fissore, Isabelle Gnaedig and Hélène Kirchner (LORIA-INRIA &
LORIA-CNRS, France)
A Logical Characterization of Efficiency
Preorders
Neelesh Korade (Persistent Systems Private Limited, India) and S.
Arun-Kumar (Indian Institute of Technology, India)
Specifying Software
Connectors
Marco Antonio Barbosa and Luís Soares Barbosa (Universidade do Minho,
Portugal)
|
|
16:00 - 18:00
|
SECTION 2B: DISTRIBUTED SYSTEMS (Chair: Jing Song Dong,
National University, Singapore)
|
|
|
A Static Analysis for Security Properties
in PKI-based Protocols
Benjamin Aziz (University College Cork, Ireland), David Gray and
Geoff Hamilton (Dublin City University, Ireland)
Decomposing Controllers into
Non-conflicting Distributed Controllers
Padmanabhan Krishnan (Bond University, Australia)
Towards an Optimization-based Method for
Consolidating Domain Variabilities in Domain-specific Web Services
Composition
Jun-feng Zhao, Lu Zhang, Ya-sha Wang, Ying Jiang and Bing Xie
(Peking University, China)
Replicative - Distribution Rules in P
Systems with Active Membranes
Tseren-Onolt Ishdorj (The State University of Education of Mongolia,
Mongolia) and Mihai Ionescu (Rovira i Virgili University, Spain)
|
THURSDAY, 23RD SEPTEMBER 2004
|
|
8:30 - 9:30
|
KEYNOTE TALK 3 (Chair: Zhiming Liu, UNU-IIST, Macao)
|
|
|
Huimin Lin, Institute of Software, Chinese Academy of Sciences, China
|
|
9:30 - 10:00
|
BREAK
|
|
10:00 - 12:00
|
SESSION 3A: AUTOMATED PROOF AND MODEL CHECKING (Chair:
Ryszard Janicki, McMaster University, Canada)
|
|
|
Idempotent Relations in
Isabelle/HOL
Florian Kammüeller (Technische Universität Berlin, Germany) and J.W.
Sanders (University of Oxford, UK)
Symbolic and Parametric Model Checking of
Discrete-Time Markov Chains
Conrado Daws (University of Twente, The Netherlands)
Verifying Linear Duration Constraints of
Timed Automata
Pham Hong Thai and Dang Van Hung (UNU-IIST, Macao)
Program Verification Using
Automatic Generation of Invariants
Enric Rodríguez-Carbonell (Technical University of Catalonia, Spain) and
Deepak Kapur (University of New Mexico, USA)
|
|
10:00 - 12:00
|
SESSION 3B: MODEL INTEGRATION AND TEHORY UNIFICATION (Chair:
Shaoying Liu, Hosei University, Japan)
|
|
|
A Formal Framework for Ontology Integration
Based on a Default Extension to DDL
Yinglong Ma, Jun Wei and Shaohua Liu (Institute of Software, Chinese
Academy of Sciences, China)
A Predicative Semantic Model for
Integrating UML Models
Jing Yang, Quan Long (UNU-IIST, Macao) and Xiaoshan Li (University
of Macau, Macao)
Automatic Mapping from Statecharts to
Verilog
Viet-Anh Vu Tran (Vietsoftware Company, Vietnam), Shengchao Qin and
Wei Ngan Chin (National University of Singapore, Singapore)
Reverse Observation Equivalence Between
Labelled State Transition Systems
Yanjun Wen, Ji Wang and Zhichang Qi (National Laboratory for Parallel and
Distributed Processing, China)
|
|
12:00 - 13:30
|
LUNCH
|
|
13:30 - 14:30
|
KEYNOTE TALK 4 (Chair: Jeff Sanders, Oxford University, UK)
|
|
|
K. Rustan M. Leino, Microsoft Research, USA
|
|
14:30 - 15:00
|
BREAK
|
|
15:00 - 17:00
|
SESSION 4A: PROGRAM TESTING AND REASONING (Chair: Hong Zhu,
Oxford Brookes University, UK)
|
|
|
An Approach to Integration Testing Based on
Data Flow Specifications
Yuting Chen, Shaoying Liu, and Fumiko Nagoya (Hosei University,
Japan)
Combining Algebraic and Model-based Test
Case Generation
Li Dan and Bernhard K. Aichernig (UNU-IIST, Macao)
Minimal Spanning Set for Coverage Testing
of Interactive Systems
Fevzi Belli and Christof J. Budnik (University of Paderborn,
Germany)
Reasoning about OWL & ORL Ontologies in
PVS
Jin Song Dong, Yu Zhang Feng and Yuan Fang Li (National University of
Singapore, Singapore)
|
|
15:00 - 17:00
|
SESSION 4B: THEORIES OF PROGRAMMING AND PROGRAMMING LANGUAGES
(Chair: Hongjun Zheng, Semantics Designs Inc, USA)
|
|
|
Random Generators for Dependent
Types
Peter Dybjer, Qiao Haiyan (Chalmers University of Technology,
Sweden) and Makoto Takeyama (National Institute of Advanced
Industrial Science and Technology, Japan)
Real Time Reactive Programming in Lucid
Enriched with Contexts
Kaiyu Wan, Vasu Alagar and Joey Paquet (Concordia University,
Canada)
A New Correctness Proof for Positive
Equality
Miroslav N. Velev (Carnegie Mellon University, USA)
Revision Programs with Explicit
Negation
Yisong Wang (Guizhou University, China) and Zhang Mingyi (Guizhou
Academy of Sciences, China)
|
|
CONFERENCE DINNER IN THE EVENING
|
FRIDAY, 24TH SEPTEMBER 2004
|
|
8:30 - 10:30
|
SESSION 5: CONCURRENCY AND MODULARITY (Chair: José Luiz
Fiadeiro, University of Leicester, UK)
|
|
|
Inherent Causal Orderings of Partial Order
Scenarios
Bill Mitchell (University of Surrey, UK)
A Generalisation of a Relational Structures
Model of Concurrency
Ryszard Janicki (McMaster University, Canada)
Nelson-Oppen, Shostak and the Extended
Canonizer: A Family Picture with a Newborn
Silvio Ranise, Christophe Ringeissen and Duc-Khanh Tran
(LORIA-INRIA, France)
Object Connectivity and Full Abstraction
for a Concurrent Calculus of Classes
Erika Ábrahám (University Freiburg, Germany), Marcello M. Bonsangue
(Univeristy Leiden, The Netherlands), Frank S. de Boer (CWI Amsterdam, The
Netherlands) and Martin Steffen (Christian-Albrechts-University Kiel,
Germany)
|
|
10:30 - 11:00
|
BREAK
|
|
11:00 - 11:30
|
CLOSING SESSION (Chair: Zhiming Liu, UNU-IIST, Macao)
|
|
11:30 - 13:00
|
LUNCH
|
|
13:00 - 20:00
|
EXCURSION
|
|