The Coq mailing list

["Farn Wang" <farn AT cc.ee.ntu.edu.tw>]

We apologize if you have received multiple copies of the announcement.

*******************************************************************************

CALL FOR PARTICIPATION

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

ATVA 2004

========

2nd International Symposium on

Automated Technology for Verification and Analysis

--------------------------------------------------------------------

National Taiwan University

Sunday 31 October - Wednesday 3 November 2004.

http://cc.ee.ntu.edu.tw/~atva04

----------------------------------------------------------------------

Encouraged by the success of the first ATVA in December 2003 and

the promise of related research and industry in East Asia,

we are very happy to announce the second ATVA. 

The emphasis of ATVA 2004 will continue to be on various mechanical

and informative techniques, which can give engineers valuable

feedbacks to quickly converge their designs according to the

specifications.  ATVA received 69 submissions. 

The final program consists of

* 3 tutorials (by Robert Kurshan of Cadence, Rajeev Alur of U.

  Pennsylvania, and Pei-Hsin Ho of Synopsys),

* 3 keynote speeches (speakers the same as for the tutorials),

* three invited speeches (by Jean-Pierre Jouannaud of Ecole

  Polytechnique, Tevfik Bultan of UCSB, and Shaoying Liu of Hosei

  Univ.),

* 24 regular papers,

* 7 special track papers,

* 8 short papers,

* a reception, a banquet and an excursion.  

The PROCEEDINGS will be available as LNCS 3299, Springer-Verlag at

ATVA 2004.  The early registration deadline is 31 September 2004.

Accomodation information is also on the ATVA 2004 webpage. 

 

ATVA 2004 will be a back-to-back occurrence with APLAS 2004

(Asian Symposium on Programming Languages and Systems, 4-6 November

2004) in Taipei. 

 

SCOPE OF INTEREST: The scope of interest includes the following

research areas: parametric analysis (parameter synthesis),

automated synthesis, optimization, performance analysis, automated

tool supports, model-checking theory, theorem-proving theory,

state-space reduction techniques, languages in automated

verification, real-time systems, embedded systems,

infinite-state systems, Petri-nets, UML, synthesis, practice in

industry, decidability and complexity issues, case studies. 

Special emphasis will be on the algorithms, complexities, tools,

and experiments of automated verification and analysis. 

 

SPECIAL TRACKS:

ATVA 2004 will also have three special tracks with independent paper

reviewing processes.  The three tracks are

(1) Design of Secure/High-reliable Networks,

(2) HW/SW Coverification and Cosynthesis, and

(3) Hardware Verification. 

KEYNOTE SPEAKERS:

Dr. Robert Kurshan (Cadence, USA)

Prof. Rajeev Alur (U. Pennsylvania, USA) 

PAPER SUBMISSION: Each submission is limited to 15 pages with no more than 5000 words. Submissions must be written in English.  The formal proceedings will be available at ATVA 2004 as a volume in LNCS, Springer-Verlag.  An accepted paper without a registered author to ATVA 2004 by the deadline of camera-ready copy will not be included in the formal proceedings.  Web-based submission is available at http://cc.ee.ntu.edu.tw/~atva04.  Extended versions of selected papers from the conference series will be solicited for publication in special issues of the International Journal of Foundations of Computer Science (IJFCS) (http://www.cs.ucsb.edu/~ijfcs).

IMPORTANT DATES:

31 May 2004, new submission deadline 

10 July 2004, acceptance notification

20 August 2004, camera-ready copy

31 October-3 November 2004, ATVA

 

ORGANIZATION

STEERING COMMITTEE:

E. A. Emerson, Oscar H. Ibarra, Insup Lee, Doron A. Peled, Farn Wang, Hsu-Chun Yen

ORGANIZING CHAIR: Hsu-Chun Yen

PROGRAM CHAIR: Farn Wang

SPECIAL TRACK CHAIRS:

(1)      Teruo Higashino (Japan)

(2)      Pao-Ann Hsiung (Taiwan)

(3)      Chung-Yang Huang, Bow-Yaw Wang (Taiwan)

PROGRAM COMMITTEE:

Tommaso Bolognesi (Italy), Tevfik Bultan (USA), Sungdeok Cha (Korea),

Yung-Ping Cheng (Taiwan), Jin-Young Choi (Korea), Jing-Song Dong (Singapore)

Jifeng He (China), Teruo Higashino (Japan), Pao-Ann Hsiung (Taiwan)

Chung-Yang Huang (Taiwan), Oscar H. Ibarra (USA), Insup Lee (USA)

Huimin Lin (China), Doron A. Peled (UK), Scott D. Stoller (USA)

Yih-Kuen Tsay (Taiwan), Bow-Yaw Wang (Taiwan), Farn Wang (Taiwan)

Hsu-Chun Yen (Taiwan), Tomohiro Yoneda (Japan)

 

--------------------------------------------------------------------------------------------

ATVA 2004 PROGRAM

--------------------------------------------------------------------------------------------

Sunday 31 October 2004

0930-1130 Tutorial I: Formal Modeling and Analysis of Hybrid Systems

          Rajeev Alur, Univ. of Pennsylvania

1130-1300 Lunch

1300-1500 Tutorial II: Assertion-Based Verification - Part A

          Bob Kurshan, Cadence

1500-1530 Break

1530-1730 Tutorial III: Assertion-Based Verification - Part B

          Pei-Hsin Ho

1830-2030 Reception

--------------------------------------------------------------------------------------------

Monday 1 November 2004

0800-0830 Registration and checking-in

0830-0840 Opening

0840-0940 Session 1: Keynote speech

          Games for Formal Design and Verification of Reactive Systems

          Rajeev Alur, U. of Pennsylvania

0940-1000 Break

1000-1200 Session 2: Model-checking (I)

       *  Toward Unbounded Model Checking for Region Automata

          Fang Yu and Bow-Yaw Wang

       *  Search Space Partition and Case Basis Exploration for Reducing Model Checking Complexity

          Bai Su, Wenhui Zhang

       *  Synthesising Attacks on Cryptographic Protocols

          David Sinclair, David Gray and Geoff Hamilton

       *  Buchi complementation made tighter

          Ehud Friedgut, Orna Kupferman, and Moshe Y. Vardi

1200-1330 Lunch

1330-1400 Session 3: Invited speech

          Tools for Automated Verification of Web services

          Tevfik Bultan, Univ. of California, Santa Barbara

1400-1530 Session 4: SAT-based techniques

       *  SAT-Based Verification of Safe Petri Nets

          Shougo Ogata, Tatsuhiro Tsuchiya, and Tohru Kikuno

       *  Disjunctive invariants for numerical systems

          Jerome Leroux

       *  Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas

          Atsushi Moritomo, Kiyoharu Hamaguchi, and Toshinobu Kashiwabara

1530-1600 Break

1600-1730 Session 5: Testing

       *  Fair Testing Revisited: a Process-Algebraic Characterisation of Conflicts

          Robi Malik, David Streader

       *  Exploiting Symmetries for Testing Equivalence in the Spi Calculus

          I. Cibrario B., L. Durante, R. Sisto, and A. ValenzanoDr.

       *  An elegant data-flow-based approach to detect concurrency errors

          Cyrille Artho and Klaus Havelund and Armin Biere

1730-1850 Session 6: Short papers

       *  Verification of WCDMA Protocols and Implementation

          Anyi Chen, Jian-Ming Wang and Chiu-Han Hsiao

       *  CLP based Static Property Checking

          Tun Li, Yang Guo, Si-Kun LiDr. 

       *  Efficient Representation of Algebraic Expressions

          Tsung Lee and P.H. Yu

       *  Development of RTOS for PLC using Formal Methods

          Jin Hyun Kim, Su-Young Lee, Young Ah Ahn, Jae Hwan Sim, Jin Seok Yang, Na Young Lee, Jin Young Choi

       *  Reducing Parameterised Automata: a Multimedia Protocol Service Case Study

          Lin Liu and Jonathan Billington

       *  Synthesis of State Feedback Controllers for Parameterized Discrete Event Systems

          Hans Bherer, Jules Desharnais, Marc Frappier, Richard St-Denis

       *  Solving Box-Pushing Games via Model Checking with Optimizations

          Gihwon Kwon, Taehoon Lee

       *  A Temporal Assertion Extension to Verilog

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

--------------------------------------------------------------------------------------------

Tuesday 2 November 4.

0830-0930 Session 7: Keynote speech

          Evolution of Model Checking into the EDA Industry

          Bob Kurshan, Cadence

0930-1000 Break

1000-1030 Session 8: Invited Speech

          Theorem proving languages for verification

          Jean-Pierre Jouannard, Ecole Polytechnique 

1030-1200 Session 9: Abstraction

       *  Abstraction-based Model Checking Using Heuristical Refinement

          Kairong Qian

       *  A Global Timed Bisimulation Preserving Abstraction for Parametric Time-Interval Automata

          Tadaaki Tanimoto, Suguru Sasaki, Akio Nakata, Teruo Higashino

       *  Design and Evaluation of a Symbolic and Abstraction-based Model Checker

          Serge Haddad, Jean-Michel Ilie and Kais Klai

          Mr. Kais Klai

1200-1300 Session 10: Industrial applications

       *  Component-wise Instruction-cache Behavior Prediction

          Abdur Rakib, Oleg Persin, Stephan Thesing, Reinhard Wilhelm

       *  Validating the Translation of an Industrial Optimizing Compiler*

          R. Leviathan Gordin, A. Pnueli

1300-1730 Lunch & picnic

1730-1830 Business meeting

1830-2030 Banquet

--------------------------------------------------------------------------------------------

Wednesday 3 November 2004

0830-0930 Session 11: Keynote speech

          Abstraction refinement

          Pei-Hsin Ho, Synopsys

0930-1000 Break

1000-1100 Session 12A: Special track I

       *  Rabin Tree and its Application to Group Key Distribution

          Hiroaki Kikuchi

       *  Using Overlay Networks to Improve VoIP Reliability

          M. Karol, P. Krishnan, and J. J. Li

1000-1100 Session 12B: Special track II

       *  An Integrity-Enhanced Verification Scheme for Software-Intensive Organizations

          Wen-Kui Chang, Chun-Yuan Chen

       *  RCGES: Retargetable Code Generation for Embedded Systems

          Trong-Yen Lee, Yang-Hsin Fan, Tsung-Hsun Yang, Chia-Chun Tsai, Wen-Ta Lee, and Yuh-Shyan Hwang

1000-1130 Session 12C: Special track III

       *  Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri Nets

          Scott Little, David Walter, Chris Myers, and Tomohiro Yoneda

       *  Localizing Errors in Counterexample with Iteratively Witness Searching

          Sheng-Yu Shen, Ying Qin, Si-Kun Li

       *  First-order LTL Model Checking using MDGs

          Fang Wang, Sofiene Tahar, Otmane Ait Mohamed

1130-1300 Lunch

1300-1330 Session 13: Invited speech

          An Automated Rigorous Review Method for Verifying and Validating Formal Specifications

          Shaoying Liu

1330-1500 Session 14: Infinite-state systems

       *  Combination of accelerations to verify infinite heterogeneous systems

          Bardin Sebastien and Alain Finkel

       *  Hybrid System Verification is not a Sinecure - The Electronic Throttle Control Case Study

          Ansgar Fehnker and Bruce H. Krogh

       *  Providing Automated Verification in HOL using MDGs

          Tarek Mhamdi and Sofiene Tahar

1500-1530 Session 15: Theorem-proving

       *  Specification, abduction, and proof

          Konstantine Arkoudas

1530-1600 Break

1600-1700 Session 16: Modelling languages 

       *  Introducing Structural Dynamic Changes in Petri Nets: Marked-Controlled Reconfigurable Nets

          Marisa Llorens and Javier OliverMs.

       *  Typeness for $\omega$-Regular Automata

          Orna Kupferman, Gila Morgenstern, and Aniello Murano

1700-1830 Session 17: Model-checking (II)

       *  Partial Order Reduction for Detecting Safety and Timing Failures of Timed Circuits

          Denduang Pradubsuwun, Tomohiro Yoneda, Chris Myers

       *  Mutation Coverage Estimation for Model Checking

          Te-Chang Lee and Pao-Ann Hsiung

       *  Modular Model Checking of Software Specifications with Simultaneously Environment Generation*

          Claudio de la Riva and Javier Tuya

1830-1900 Closing