2. ATVA 2004:
Taipei,
Taiwan
Farn Wang (Ed.):
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
Invited Speech
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
Last update Tue Feb 14 03:49:15 2012
CET by the DBLP Team —
Data released under the ODC-BY 1.0 license — See also our legal information page