From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: * X-Spam-Status: No, score=1.9 required=5.0 tests=AWL,HTML_10_20,HTML_MESSAGE, SPF_SOFTFAIL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id DD161BBAF for ; Thu, 4 Jun 2009 19:52:41 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Aq0GAKGmJ0qB6ggVnGdsb2JhbACCIDKVTQEBAQEBCAsICRG3XoQLBYhI X-IronPort-AV: E=Sophos;i="4.41,306,1241388000"; d="scan'208,217";a="27354283" Received: from hermes2.dur.ac.uk ([129.234.8.21]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 04 Jun 2009 19:52:41 +0200 Received: from DURMAIL3.mds.ad.dur.ac.uk (durmail3a.dur.ac.uk [129.234.8.189]) by hermes2.dur.ac.uk (8.13.8/8.13.7) with ESMTP id n54Hl1VW026349; Thu, 4 Jun 2009 18:47:05 +0100 X-MimeOLE: Produced By Microsoft Exchange V6.5 Content-class: urn:content-classes:message MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="----_=_NextPart_001_01C9E53C.97DA9FE8" Subject: TASE 2009 - Call for Participation Date: Thu, 4 Jun 2009 18:43:55 +0100 Message-ID: <8405C0D818720A45A8C69862358075EE03E3F0@DURMAIL3.mds.ad.dur.ac.uk> X-MS-Has-Attach: X-MS-TNEF-Correlator: Thread-Topic: TASE 2009 - Call for Participation Thread-Index: AcnDbBk99bSitWU8T5S5cBq7l/Hjighz+7vR References: <8405C0D818720A45A8C69862358075EE03E3E4@DURMAIL3.mds.ad.dur.ac.uk> From: "CRACIUN F." To: , , , , , , , , , , , , , , , , , , , Cc: "IEEE-TASE-2009 C.S." X-DurhamAcUk-MailScanner-ID: n54Hl1VW026349 X-DurhamAcUk-MailScanner: Found to be clean X-Spam: no; 0.00; zhong:01 shao:01 semantics:01 arne:01 semantics:01 unifying:01 algebra:01 iist:01 iist:01 model:01 abstraction:01 bounded:01 model:01 modular:01 zhong:01 This is a multi-part message in MIME format. ------_=_NextPart_001_01C9E53C.97DA9FE8 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable TASE 2009 - CALL FOR PARTICIPATION ********************************************************** * 3rd IEEE International Symposium on * Theoretical Aspects of Software Engineering * (TASE 2009) * 29-31 July 2009, Tianjin, China * http://www.dur.ac.uk/ieee.tase2009 * * Early Registration Deadline : 18 June 2009 * For more information email: IEEE.TASE2009@durham.ac.uk ***********************=3D********************************** TASE 2009 Invited Speakers =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D Kim G. Larsen, Aalborg University, Denmark Zhong Shao, Yale University, USA =20 Jin-Song Dong, National University of Singapore =20 =20 TASE 2009 Programme =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D Day 1: 29 July 2009 ------------------- Invited Talk: Verification and Performance Analysis of Embedded Systems Kim G. Larsen (Aalborg University) Session 1 : Real-Time and Embedded Systems Improving Responsiveness of Hard Real-Time Embedded Systems Hugh Anderson (Wellington Institute of Technology) and Siau-Cheng KHOO = (National University of Singapore) =20 Environmental Simulation of Real-Time Systems with Nested Interrupts Guoqiang Li (Shanghai Jiao Tong University), Shoji Yuen (Nagoya = University) and Masakazu Adachi (Toyota Central R&D Labs. INC.).=20 Semantics for Communicating Actors with Interdependent Real-Time = Deadlines Istv=A8=A2n Knoll (Aalborg University), Anders P. Ravn (Aalborg = University) and Arne Skou (Aalborg University).=20 An Efficient Algorithm for Finding Empty Space for Reconfigurable = Systems Zhenhua Duan (Xidian University) and Yan Xiao (Xidian University).=20 Session 2 : Semantics State Visibility and Communication in Unifying Theories of Programming Andrew Butterfield (Trinity College Dublin), Pawel Gancarski (Trinity = College Dublin) and Jim Woodcock (University of York).=20 Semantics of Metamodels in UML Lijun Shan (National University of Defence Technology) and Hong Zhu = (Oxford Brookes University).=20 Refinement Algebra with Explicit Probabilism Tahiry Rabehaja (UNU/IIST) and Jeffrey Sanders (UNU/IIST).=20 Session 3 : Model Checking Environment Abstraction with State Clustering and Parameter Truncating Hong Pan (Institute of Software, Chinese Academy of Sciences), Yi Lv = (Institute of Software, Chinese Academy of Sciences) and Huimin Lin = (Institute of Software, Chinese Academy of Sciences).=20 Verification of Population Ring Protocols in PAT Yang Liu (National University of Singapore), Jun Pang (University of = Luxembourg), Jun Sun (National University of Singapore) and Jianhua Zhao = (Nanjing University).=20 Bounded Model Checking of ACTL Formulae Wei Chen (Institute of Software, Chinese Academy of Sciences) and Wenhui = Zhang (Institute of Software, Chinese Academy of Sciences).=20 Day 2, 30 July 2009 ------------------- Invited Talk: Modular Development of Certified System Software Zhong Shao (Yale University) =20 Session 4: Specification and Security Coarse Grained Retrenchment and the Mondex Denial of Service Attacks Richard Banach (Manchester University).=20 Specifying and Enforcing Constraints of Artifact Life Cycles Xiangpeng Zhao (Peking University), Jianwen Su (University of California = at Santa Barbara), Hongli Yang (Beijing University of Technology) and = Zongyan Qiu (Peking University).=20 Consistency Checking for LSC Specifications Hai-Feng Guo (University of Nebraska at Omaha), Wen Zheng (University of = Nebraska at Omaha) and Mahadevan Subramaniam (University of Nebraska at = Omaha).=20 Integrating Specification and Programs for System Modeling and = Verification Jun Sun (National University of Singapore), Yang Liu (National = University of Singapore), Jin Song Dong (National University of = Singapore) and Chunqing Chen (National University of Singapore).=20 Session 5 : Software Testing I A Framework and Language Support for Automatic Dynamic Testing of = Workflow Management Systems Gwan-Hwan Hwang (National Taiwan Normal University), Che-Sheng Lin = (National Taiwan Normal University), Li-Te Tsao (National Taiwan Normal = University), Kuei-Huan Chen (National Taiwan Normal University) and = Yan-You Li (National Taiwan Normal University).=20 Fault-based Test Case Generation for Component Connectors Bernhard Aichernig (Graz University of Technology), Farhad Arbab (CWI), = Lacramioara Astefanoaei (CWI), Frank de Boer (CWI), Meng Sun (CWI) and = Jan Rutten (CWI).=20 Test Data Generation for Derived Types in C Program Zheng Wang (East China Normal University), Xiao Yu (East China Normal = University), Tao Sun (East China Normal University), Geguang Pu (East = China Normal University) and Zuohua Ding (Zhejiang Sci-Tech University). = Session 6 : Software Models Program Repair as Sound Optimization of Broken Programs=20 Bernd Fischer (University of Southampton), Ando Saabas (Tallinn = University of Technology) and Tarmo Uustalu (Tallinn University of = Technology).=20 Modeling Web Applications and Generating Tests: A Combination and = Interactions-guided Approach=20 Bo Song (Shanghai University) and Huaikou Miao (Shanghai University).=20 Merging of Use Case Models: Semantic Foundations =20 Stephen Barrett (Concordia University), Daniel Sinnig (Concordia = University), Patrice Chalin (Concordia University) and Greg Butler = (Concordia University).=20 Day 3, 31 July 2009 ------------------- Invited Tutorial: Towards Expressive Specification and Efficient Model Checking Jin Song Dong (National University of Singapore) Session 7 : Verification Verifying Semistructured Data Normalization using SWRL Yuan Fang Li (University of Queensland), Jing Sun (University of = Auckland), Gillian Dobbie (University of Auckland), Scott Uk-Jin Lee = (University of Auckland) and Hai H. Wang (Aston University).=20 Verifying Self-stabilizing Population Protocols with Coq Yuxin Deng (Shanghai Jiao Tong University) and Jean-fran?ois Monin = (Universit=A8=A6 de Grenoble 1). The Logical Approach to Low-level Stack Reasoning Xinyu Jiang (University of Science and Technology of China), Yu Guo = (University of Science and Technology of China) and Yiyun Chen = (University of Science and Technology of China).=20 Constructing Program Invariants via Solving QBF Shikun Chen (National University of Defence Technology), Zhoujun Li = (Beihang University) and Mengjun Li (National University of Defence = Technology).=20 Session 8 : Concurrency=20 Using Architectural Constraints for Deadlock-Freedom of Component = Systems with Multiway Cooperation Moritz Martens (University of Mannheim) and Mila Majster-Cederbaum = (University of Mannheim).=20 Formal Reasoning about Concurrent Assembly Code with Reentrant Locks Ming Fu (University of Science and Technology of China), Yu Zhang = (University of Science and Technology of China) and Yong Li (University = of Science and Technology of China).=20 Algorithms for Computing Weak Bisimulation Equivalence Weisong Li (Institute of Software, Chinese Academy of Sciences).=20 Session 9 : Software Testing II Interpreting a Successful Testing Process: Risk and Actual Coverage Marielle Stoelinga (University of Twente) and Mark Timmer (University of = Twente).=20 Automated Test Case Generation based on Coverage Analysis Tim A. Majchrzak (University of Muenster) and Herbert Kuchen (University = of Muenster).=20 Exploring Topological Structure of Boolean Expressions for Test Data = Selection Lian Yu (Peking University), Wei Zhao (IBM China Research Lab), = Xiangdong Fan (Peking University) and Jun Zhu (IBM China Research Lab).=20 On Testing 1-Safe Petri Nets Guy-Vincent Jourdan (University of Ottawa) and Gregor von Bochmann = (University of Ottawa).=20 The programme also include two poster sessions, comprising of 23 selected poster presentations. This list of posters can=20 be found at http://www.dur.ac.uk/ieee.tase2009/ =20 ------_=_NextPart_001_01C9E53C.97DA9FE8 Content-Type: text/html; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable TASE 2009 - Call for Participation

        TASE 2009 - = CALL FOR PARTICIPATION

**********************************************************
*    3rd IEEE International Symposium on
* Theoretical Aspects of Software Engineering
*            = (TASE 2009)
*     29-31 July 2009, Tianjin, China
*    http://www.dur.ac.uk/ieee.tas= e2009
*
* Early Registration Deadline : 18 June 2009
* For more information email: IEEE.TASE2009@durham.ac.uk
***********************=3D**********************************


TASE 2009 Invited Speakers
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D

Kim G. Larsen, Aalborg University, Denmark

Zhong Shao, Yale University, USA

Jin-Song Dong, National University of Singapore



TASE 2009 Programme
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D

Day 1: 29 July 2009
-------------------

Invited Talk:

Verification and Performance Analysis of Embedded Systems
Kim G. Larsen (Aalborg University)

Session 1 : Real-Time and Embedded Systems

Improving Responsiveness of Hard Real-Time Embedded Systems
Hugh Anderson (Wellington Institute of Technology) and Siau-Cheng KHOO = (National University of Singapore) 

Environmental Simulation of Real-Time Systems with Nested Interrupts
Guoqiang Li (Shanghai Jiao Tong University), Shoji Yuen (Nagoya = University) and Masakazu Adachi (Toyota Central R&D Labs. INC.).

Semantics for Communicating Actors with Interdependent Real-Time = Deadlines
Istv=A8=A2n Knoll (Aalborg University), Anders P. Ravn (Aalborg = University) and Arne Skou (Aalborg University).

An Efficient Algorithm for Finding Empty Space for Reconfigurable = Systems
Zhenhua Duan (Xidian University) and Yan Xiao (Xidian University).

Session 2 : Semantics

State Visibility and Communication in Unifying Theories of = Programming
Andrew Butterfield (Trinity College Dublin), Pawel Gancarski (Trinity = College Dublin) and Jim Woodcock (University of York).

Semantics of Metamodels in UML
Lijun Shan (National University of Defence Technology) and Hong Zhu = (Oxford Brookes University).

Refinement Algebra with Explicit Probabilism
Tahiry Rabehaja (UNU/IIST) and Jeffrey Sanders (UNU/IIST).

Session 3 : Model Checking

Environment Abstraction with State Clustering and Parameter = Truncating
Hong Pan (Institute of Software, Chinese Academy of Sciences), Yi Lv = (Institute of Software, Chinese Academy of Sciences)  and Huimin = Lin (Institute of Software, Chinese Academy of Sciences).

Verification of Population Ring Protocols in PAT
Yang Liu (National University of Singapore), Jun Pang (University of = Luxembourg), Jun Sun (National University of Singapore) and Jianhua Zhao = (Nanjing University).

Bounded Model Checking of ACTL Formulae
Wei Chen (Institute of Software, Chinese Academy of Sciences) and Wenhui = Zhang (Institute of Software, Chinese Academy of Sciences).

Day 2, 30 July 2009
-------------------

Invited Talk:

Modular Development of Certified System Software
Zhong Shao (Yale University) 

Session 4: Specification and Security

Coarse Grained Retrenchment and the Mondex Denial of Service Attacks
Richard Banach (Manchester University).

Specifying and Enforcing Constraints of Artifact Life Cycles
Xiangpeng Zhao (Peking University), Jianwen Su (University of California = at Santa Barbara), Hongli Yang (Beijing University of Technology) and = Zongyan Qiu (Peking University).

Consistency Checking for LSC Specifications
Hai-Feng Guo (University of Nebraska at Omaha), Wen Zheng (University of = Nebraska at Omaha) and Mahadevan Subramaniam (University of Nebraska at = Omaha).

Integrating Specification and Programs for System Modeling and = Verification
Jun Sun (National University of Singapore), Yang Liu (National = University of Singapore), Jin Song Dong (National University of = Singapore) and Chunqing Chen (National University of Singapore).

Session 5 : Software Testing I

A Framework and  Language Support for Automatic Dynamic Testing of = Workflow Management Systems
Gwan-Hwan Hwang (National Taiwan Normal University), Che-Sheng Lin = (National Taiwan Normal University), Li-Te Tsao (National Taiwan Normal = University), Kuei-Huan Chen (National Taiwan Normal University) and = Yan-You Li (National Taiwan Normal University).

Fault-based Test Case Generation for Component Connectors
Bernhard Aichernig (Graz University of Technology), Farhad Arbab (CWI), = Lacramioara Astefanoaei (CWI), Frank de Boer (CWI), Meng Sun (CWI) and = Jan Rutten (CWI).

Test Data Generation for Derived Types in C Program
Zheng Wang (East China Normal University), Xiao Yu (East China Normal = University), Tao Sun (East China Normal University), Geguang Pu (East = China Normal University) and Zuohua Ding (Zhejiang Sci-Tech = University).

Session 6 : Software Models

Program Repair as Sound Optimization of Broken Programs
Bernd Fischer (University of Southampton), Ando Saabas (Tallinn = University of Technology) and Tarmo Uustalu (Tallinn University of = Technology).

Modeling Web Applications and Generating Tests: A Combination and = Interactions-guided Approach
Bo Song (Shanghai University) and Huaikou Miao (Shanghai = University).

Merging of Use Case Models: Semantic Foundations 
Stephen Barrett (Concordia University), Daniel Sinnig (Concordia = University), Patrice Chalin (Concordia University) and Greg Butler = (Concordia University).

Day 3, 31 July 2009
-------------------

Invited Tutorial:

Towards Expressive Specification and Efficient Model Checking
Jin Song Dong (National University of Singapore)

Session 7 : Verification

Verifying Semistructured Data Normalization using SWRL
Yuan Fang Li (University of Queensland), Jing Sun (University of = Auckland), Gillian Dobbie (University of Auckland), Scott Uk-Jin Lee = (University of Auckland)  and Hai H. Wang (Aston University).

Verifying Self-stabilizing Population Protocols with Coq
Yuxin Deng (Shanghai Jiao Tong University) and Jean-fran?ois Monin = (Universit=A8=A6 de Grenoble 1).

The Logical Approach to Low-level Stack Reasoning
Xinyu Jiang (University of Science and Technology of China), Yu Guo = (University of Science and Technology of China) and Yiyun Chen = (University of Science and Technology of China).

Constructing Program Invariants via Solving QBF
Shikun Chen (National University of Defence Technology), Zhoujun Li = (Beihang University) and Mengjun Li (National University of Defence = Technology).

Session 8 : Concurrency

Using Architectural Constraints for Deadlock-Freedom of Component = Systems with Multiway Cooperation
Moritz Martens (University of Mannheim) and Mila Majster-Cederbaum = (University of Mannheim).

Formal Reasoning about Concurrent Assembly Code with Reentrant Locks
Ming Fu (University of Science and Technology of China), Yu Zhang = (University of Science and Technology of China) and Yong Li (University = of Science and Technology of China).

Algorithms for Computing Weak Bisimulation Equivalence
Weisong Li (Institute of Software, Chinese Academy of Sciences).

Session 9 : Software Testing II

Interpreting a Successful Testing Process: Risk and Actual Coverage
Marielle Stoelinga (University of Twente) and Mark Timmer (University of = Twente).

Automated Test Case Generation based on Coverage Analysis
Tim A. Majchrzak (University of Muenster) and Herbert Kuchen (University = of Muenster).

Exploring Topological Structure of Boolean Expressions for Test Data = Selection
Lian Yu (Peking University), Wei Zhao (IBM China Research Lab), = Xiangdong Fan (Peking University) and Jun Zhu (IBM China Research = Lab).

On Testing 1-Safe Petri Nets
Guy-Vincent Jourdan (University of Ottawa) and Gregor von Bochmann = (University of Ottawa).


The programme also include two poster sessions, comprising
of 23 selected poster presentations. This list of posters can
be found at http://www.dur.ac.uk/ieee.ta= se2009/

------_=_NextPart_001_01C9E53C.97DA9FE8--