[TYPES] FORTE 2005: Preliminary Program and the 1st Call for Participation

[Farn Wang]

** We apologize if you have received multiple copies of this email. ** 

 

Dear colleagues: 

 

FORTE 2005 is now cordially inviting your participation.  

This year, FORTE 2005 and ATVA 2005 are collocated with a 2-day overlapping.  

We should have a lot of people coming to the beautiful campus of National Taiwan University.  

For more information, please check out our webpage at http://cc.ee.ntu.edu.tw/~forte05.  

In the following, please find the preliminary program. 

 

Best regards, 

 

Farn Wang, Program Chair of FORTE 

2005/7/25

 

================================================================

FORTE 2005

PRELIMINARY PROGRAM 

====================================================

Sunday, Oct. 2, 2005

0830-0900: Registration

0900-1100: Tutorial (I) 

              Title: to be announced

              Speaker: Rance Cleaveland 

1100-1130: Coffee break

1130-1230: Tutorial (II) Part 1

              Title: to be announced  

              Speaker: Constance Heitmeyer 

1230-1400: Lunch

1400-1500: Tutorial (II) Part 2

              Title: to be announced  

              Speaker: Constance Heitmeyer 

1500-1530: Coffee break

1530-1730: Tutorial (III)

              Title: to be announced  

              Speaker: Teruo Higashino 

1830-2030: Reception

====================================================

Monday, Oct. 3, 2005

0800-0830: Registration

0830-0900: 

SESSION 1: Opening and welcome speeches 

0900-1000: 

SESSION 2: Keynote speech (I) 

   Developing High Quality Software with Formal Methods:  What Else Is Needed?

   Constance Heitmeyer 

1000-1030: Break 

1030-1200: 

SESSION 3: Languages and Semantics (I) 

  A COMPOSITION OPERATOR FOR SYSTEMS WITH ACTIVE AND PASSIVE ACTIONS

    Stefan Strubbe, Rom Langerak

  A FORMAL SEMANTICS OF UML STATECHARTS BY MEANS OF TIMED PETRI NETS

    Youcef HAMMAL

  A HIERARCHY OF IMPLEMENTABLE MSC LANGUAGES

    Benedikt Bollig, Martin Leucker

1200-1330: Lunch 

1330-1500: 

SESSION 4: Model-checking (I) 

  COMBONING STATIC ANALYSIS AND MODEL CHECKING FOR SYSTMES EMPLOYING

  COMMUTATIVE FUNCTIONS

    A. Prasad Sistla, Min Zhou

  FAST GENERIC MODEL-CHECKING FOR DATA-BASED SYSTEMS

    Dezhuang Zhang Rance Cleaveland

  LOGIC AND MODEL CHECKING FOR HIDDEN MARKOV MODELS

    Lijun Zhang, Holger Hermanns, David N. Jansen

1500-1530: 

SESSION 5: SAT-based techniques 

  PROVING \FORALL\MU-CALCULUS PROPERTIES WITH SAT SOLVERS

    Bow-Yaw Wang

1530-1600: Coffee break 

1600-1730: 

SESSION 6: Protocol verification 

  AD HOC ROUTING PROTOCOL VERIFICATION THROUGH BROADCAST ABSTRACTION

    Oskar Wibling, Joachim Parrow, Arnold Pears

  DISCOVERING CHATTER AND INCOMPLETENESS IN THE DATAGRAM CONGESTION

  CONTROL PROTOCOL

    Somsak Vanit-Anunchai, Jonathan Billington, Tul Kongprakaiwoot

  THREAD ALLOCATION PROTOCOLS FOR DISTRIBUTED REAL-TIME AND EMBEDDED

  SYSTEMS

    Cesar Sanchez, Henny B. Sipma, Venkita Subramonian, Christopher Gill, 

    Zohar Manna

1730-1830: 

SESSION 7: Petri nets

  A PETRI NET VIEW OF MOBILITY

    Charles Lakos

  MODULAR VERIFICATION OF PETRI NETS PROPERTIES: A STRUCTURE-BASED

  APPROACH

    Kais Klai, Serge Haddad, Jean-Michel Ili?

====================================================

Tuesday, Oct. 4, 2005

0830-0930: 

SESSION 8: Keynote speech (II) 

  A Testing Architecture for Designing High-Reliable MANET Protocols

   Teruo Higashino 

0930-1000: Break 

1000-1100: 

SESSION 9: Testing 

  AN IMPROVED CONFORMANCE TESTING METHOD

    Rita Dorofeeva, Khaled El-Fakih, Nina Yevtushenko

  RESOLVING OBSERVABILITY PROBLEMS IN DISTRIBUTED TEST ARCHITECTURES

    Jessica Chen, Robert M. Hierons, Hasan Ural

1100-1200:

SESSION 10: Security systems 

  AUTOMATIC GENERATION OF CONFLICT-FREE IPSEC POLICIES

    Chi-Lam Chang, Yun-Peng Chiu, Chin-Laung Lei

  A FRAMEWORK BASED APPROACH FOR FORMAL MODELING AND ANALYSIS OF

  MULTI-LEVEL ATTACKS IN COMPUTER NETWORKS

    Gerrit Rothmaier, Heiko Krumm

1200-1330: Lunch and Business Meeting 

1330-1500: 

SESSION 11: Model-checking (II) 

  MODEL CHECKING FOR TIMED STATECHARTS

    Junyan Qian, Baowen Xu

  ABSTRACTION-GUIDED MODEL CHECKING USING SYMBOLIC IDA* AND HEURISTIC

  SYNTHESIS

   Kairong Qian Albert Nymeyer Steven Susanto

  MODELING AND VERIFICATION OF SAFETY-CRITICAL SYSTEMS USING SAFECHARTS

    Pao-Ann Hsiung, Yen-Hung Lin

1500-1530: 

SESSION 12: Abstraction 

  STRUCTURE PRESERVING DATA ABSTRACTIONS FOR STATECHARTS

    Steffen Helke, Florian Kammler

1530-1600: Coffee break 

1600-1730: 

SESSION 13: Fundamentals 

  AMORTISED BISIMULATIONS

    Astrid Kiehn, S. Arun-Kumar

  PROOF METHODOLOGIES FOR BEHAVIOURAL EQUIVALENCE IN DISTRIBUTED

  PI-CALCULUS

    Alberto Ciaffaglione, Matthew Hennessy, Julian Rathke

  DERIVING NON-DETERMINISM FROM CONJUNCTION AND DISJUNCTION

    Naijun Zhan, Mila Majster-Cederbaum

1730-1830: 

SESSION 14: Languages and Semantics (II) 

  ABSTRACT OPERATIONAL SEMANTICS FOR USE CASE MAPS

    Jameleddine Hassine, Juergen Rilling, Rachida Dssouli

  ARCHITRIO: A UML-COMPATIBLE LANGUAGE FOR ARCHITECTURAL DESCRIPTION AND

  ITS FORMAL SEMANTICS

    Matteo Pradella, Matteo Rossi, Dino Mandrioli

1830-1900: Bus ride to the banquet 

1900-2130: Banquet (colocated with ATVA 2005 reception) 

====================================================

Wednesday, Oct. 5, 2005

0830-0930: 

SESSION 15: Joint keynote speech with ATVA 2005

  Ranking Abstraction as Companion to Predicate Abstraction

    Amir Pnueli 

0930-1000: Coffee break 

1000-1130: 

SESSION 16A: Synthesis

  SUBMODULE CONSTRUCTION FOR EXTENDED STATE MACHINE MODELS

    Bassel Daou, Gregor von Bochmann

  SYNCHRONIZING COLLABORATIVE OBJECTS WITH OPERATIONAL TRANSFORMATION

    Abdessamad Imine, Pascal Molli, G\'erald Oster, 

    Micha\"el Rusinowitch

  DESIGNING EFFICIENT FAIL-SAFE MULTITOLERANT SYSTEMS

    Arshad Jhumka, Neeraj Suri

1130-1200: 

SESSION 17A: Data-structures

  HIERARCHICAL DECISION DIAGRAMS TO EXPLOIT MODEL STRUCTURE

    Jean-Michel Couvreur, Yann Thierry-Mieg

1000-1130: 

SESSION 16B: New challenges in network analysis

  COMPUTING SUBGRAPH PROBABILITY OF RANDOM GEOMETRIC GRAPHS: QUANTITATIVE

  ANALYSES OF WIRELESS AD HOC NETWORKS

    Chang Wu Yu, Li-Hsing Yen

  FORMALISING WEB SERVICES

    Kenneth J. Turner

  FROM AUTOMATA NETWORKS TO HMSCS: A REVERSE MODEL ENGINEERING

  PERSPECTIVE

    Thomas Chatain, Lo騃 H幨ou褮, Claude Jard

1130-1200: 

SESSION 17B: Process Algebra 

  PROPERTIES AS PROCESSES: THEIR SPECIFICATION AND VERIFICATION

    Joel Kelso George Milne

1200-1230: Coffee break 

1230-1330: 

SESSION 18: Short papers

  AUTOMATIC PARTITIONER FOR DISTRIBUTED PARALLEL LOGIC SIMULATION

    Kai-Hui Chang, Han-Wei Wang, Wei-Ting Tu, Yi-Jong Yeh, Sy-Yen Kuo

  COMPOSITIONAL MODELLING AND VERIFICATION OF IPV6 MOBILITY

    Peng Wu, Dongmei Zhang

  EXPRESSIVE COMPLETENESS OF AN EVENT-PATTERN REACTIVE PROGRAMMING

  LANGUAGE

    Cesar Sanchez, Matteo Slanina, Henny B. Sipma, Zohar Manna

  HIERARCHICAL PROTOCOL DESCRIPTION AND TEST GENRATION METHOD FOR MOBILE

  IPV6 TESTING

    Yujun Zhang

  MODEL BUILDING AND MODEL CHECKING UNDER LARGE-SCALE DISTRIBUTED

  INTERACTION

    Horst F. Wedde, Arnim Wedig, Anca Lazarescu, Ralf Paaschen, Elisei Rotaru

  THE INDUCTIVE APPROACH TO STRAND SPACE

    Li yongjian

1400-1800: Excursion (Joint action with ATVA 2005) 

1830-2030: PC meeting