


default search action
2nd ATVA 2004: Taipei, Taiwan
- Farn Wang:

Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3, 2004. Proceedings. Lecture Notes in Computer Science 3299, Springer 2004, ISBN 3-540-23610-4
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 W. 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, Parameshwaran 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

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














