[TYPES] ATVA 2004 - Call for Participation & Program
Farn Wang
farn at cc.ee.ntu.edu.tw
Thu Sep 9 16:20:44 EDT 2004
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
More information about the Types-list
mailing list