2. ATVA 2004: Taipei, Taiwan

Keynote Speech

• Rajeev Alur:
  Games for Formal Design and Verification of Reactive Systems. 1
  
• Robert P. Kurshan:
  Evolution of Model Checking into the EDA Industry. 2-6
  
• Pei-Hsin Ho:
  Abstraction Refinement. 7
  

Invited Speech

• Tevfik Bultan, Xiang Fu, Jianwen Su:
  Tools for Automated Verification of Web Services. 8-10
  
• Jean-Pierre Jouannaud:
  Theorem Proving Languages for Verification. 11-14
  
• Shaoying Liu:
  An Automated Rigorous Review Method for Verifying and Validating Formal Specifications. 15-19
  

Papers

• Fang Yu, Bow-Yaw Wang:
  Toward Unbounded Model Checking for Region Automata. 20-33
  
• Bai Su, Wenhui Zhang:
  Search Space Partition and Case Basis Exploration for Reducing Model Checking Complexity. 34-48
  
• David Sinclair, David Gray, Geoff Hamilton:
  Synthesising Attacks on Cryptographic Protocols. 49-63
  
• Ehud Friedgut, Orna Kupferman, Moshe Y. Vardi:
  Büchi Complementation Made Tighter. 64-78
  
• Shougo Ogata, Tatsuhiro Tsuchiya, Tohru Kikuno:
  SAT-Based Verification of Safe Petri Nets. 79-92
  
• Jérôme Leroux:
  Disjunctive Invariants for Numerical Systems. 93-107
  
• Atsushi Moritomo, Kiyoharu Hamaguchi, Toshinobu Kashiwabara:
  Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas. 108-119
  
• Robi Malik, David Streader, Steve Reeves:
  Fair Testing Revisited: A Process-Algebraic Characterisation of Conflicts. 120-134
  
• Ivan Cibrario Bertolotti, Luca Durante, Riccardo Sisto, Adriano Valenzano:
  Exploiting Symmetries for Testing Equivalence in the Spi Calculus. 135-149
  
• Cyrille Artho, Klaus Havelund, Armin Biere:
  Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors. 150-164
  
• Kairong Qian, Albert Nymeyer:
  Abstraction-Based Model Checking Using Heuristical Refinement. 165-178
  
• Tadaaki Tanimoto, Suguru Sasaki, Akio Nakata, Teruo Higashino:
  A Global Timed Bisimulation Preserving Abstraction for Parametric Time-Interval Automata. 179-195
  
• Serge Haddad, Jean-Michel Ilié, Kais Klai:
  Design and Evaluation of a Symbolic and Abstraction-Based Model Checker. 196-210
  
• Abdur Rakib, Oleg Parshin, Stephan Thesing, Reinhard Wilhelm:
  Component-Wise Instruction-Cache Behavior Prediction. 211-229
  
• I. Gordin, Raya Leviathan, Amir Pnueli:
  Validating the Translation of an Industrial Optimizing Compiler. 230-247
  
• Sébastien Bardin, Alain Finkel:
  Composition of Accelerations to Verify Infinite Heterogeneous Systems. 248-262
  
• Ansgar Fehnker, Bruce H. Krogh:
  Hybrid System Verification Is Not a Sinecure: The Electronic Throttle Control Case Study. 263-277
  
• Tarek Mhamdi, Sofiène Tahar:
  Providing Automated Verification in HOL Using MDGs. 278-293
  
• Konstantine Arkoudas:
  Specification, Abduction, and Proof. 294-309
  
• Marisa Llorens, Javier Oliver:
  Introducing Structural Dynamic Changes in Petri Nets: Marked-Controlled Reconfigurable Nets. 310-323
  
• Orna Kupferman, Gila Morgenstern, Aniello Murano:
  Typeness for omega-Regular Automata. 324-338
  
• Denduang Pradubsuwun, Tomohiro Yoneda, Chris J. Myers:
  Partial Order Reduction for Detecting Safety and Timing Failures of Timed Circuits. 339-353
  
• Te-Chang Lee, Pao-Ann Hsiung:
  Mutation Coverage Estimation for Model Checking. 354-368
  
• Claudio de la Riva, Javier Tuya:
  Modular Model Checking of Software Specifications with Simultaneous Environment Generation. 369-383
  
• Hiroaki Kikuchi:
  Rabin Tree and Its Application to Group Key Distribution. 384-391
  
• Mark J. Karol, P. Krishnan, J. Jenny Li:
  Using Overlay Networks to Improve VoIP Reliability. 392-401
  
• Wen-Kui Chang, Chun-Yuan Chen:
  Integrity-Enhanced Verification Scheme for Software-Intensive Organizations. 402-414
  
• Trong-Yen Lee, Yang-Hsin Fan, Tsung-Hsun Yang, Chia-Chun Tsai, Wen-Ta Lee, Yuh-Shyan Hwang:
  RCGES: Retargetable Code Generation for Embedded Systems. 415-425
  
• Scott Little, David Walter, Nicholas Seegmiller, Chris J. Myers, Tomohiro Yoneda:
  Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri Nets. 426-440
  
• Fang Wang, Sofiène Tahar, Otmane Aït Mohamed:
  First-Order LTL Model Checking Using MDGs. 441-455
  
• ShengYu Shen, Ying Qin, Sikun Li:
  Localizing Errors in Counterexample with Iteratively Witness Searching. 456-469
  
• Anyi Chen, Jian-Ming Wang, Chiu-Han Hsiao:
  Verification of WCDMA Protocols and Implementation. 470-473
  
• Tsung Lee, Pen-Ho Yu:
  Efficient Representation of Algebraic Expressions. 474-478
  
• Jin Hyun Kim, Su-Young Lee, Young Ah Ahn, Jae-Hwan Sim, Jin Seok Yang, Na-Young Lee, Jin-Young Choi:
  Development of RTOS for PLC Using Formal Methods. 479-482
  
• Lin Liu, Jonathan Billington:
  Reducing Parametric Automata: A Multimedia Protocol Service Case Study. 483-486
  
• Hans Bherer, Jules Desharnais, Marc Frappier, Richard St.-Denis:
  Synthesis of State Feedback Controllers for Parameterized Discrete Event Systems. 487-490
  
• Gihwon Kwon, Taehoon Lee:
  Solving Box-Pushing Games via Model Checking with Optimizations. 491-494
  
• Tun Li, Yang Guo, Sikun Li:
  CLP Based Static Property Checking. 495-498
  
• Kai-Hui Chang, Wei-Ting Tu, Yi-Jong Yeh, Sy-Yen Kuo:
  A Temporal Assertion Extension to Verilog. 499-504