Automated Technology for Verification and Analysis Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31 - November 3, 2004. Proceedings / edited by Farn Wang.

Saved in:
Bibliographic Details
Corporate Author: SpringerLink (Online service)
Other Authors: Wang, Farn (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2004.
Edition:1st ed. 2004.
Series:Lecture Notes in Computer Science, 3299
Springer eBook Collection.
Subjects:
Online Access:Click to view e-book
Holy Cross Note:Loaded electronically.
Electronic access restricted to members of the Holy Cross Community.
Table of Contents:
  • Keynote Speech
  • Games for Formal Design and Verification of Reactive Systems
  • Evolution of Model Checking into the EDA Industry
  • Abstraction Refinement
  • Invited Speech
  • Tools for Automated Verification of Web Services
  • Theorem Proving Languages for Verification
  • An Automated Rigorous Review Method for Verifying and Validating Formal Specifications
  • Papers
  • Toward Unbounded Model Checking for Region Automata
  • Search Space Partition and Case Basis Exploration for Reducing Model Checking Complexity
  • Synthesising Attacks on Cryptographic Protocols
  • Büchi Complementation Made Tighter
  • SAT-Based Verification of Safe Petri Nets
  • Disjunctive Invariants for Numerical Systems
  • Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas
  • Fair Testing Revisited: A Process-Algebraic Characterisation of Conflicts
  • Exploiting Symmetries for Testing Equivalence in the Spi Calculus
  • Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors
  • Abstraction-Based Model Checking Using Heuristical Refinement
  • A Global Timed Bisimulation Preserving Abstraction for Parametric Time-Interval Automata
  • Design and Evaluation of a Symbolic and Abstraction-Based Model Checker
  • Component-Wise Instruction-Cache Behavior Prediction
  • Validating the Translation of an Industrial Optimizing Compiler
  • Composition of Accelerations to Verify Infinite Heterogeneous Systems
  • Hybrid System Verification Is Not a Sinecure
  • Providing Automated Verification in HOL Using MDGs
  • Specification, Abduction, and Proof
  • Introducing Structural Dynamic Changes in Petri Nets: Marked-Controlled Reconfigurable Nets
  • Typeness for ?-Regular Automata
  • Partial Order Reduction for Detecting Safety and Timing Failures of Timed Circuits
  • Mutation Coverage Estimation for Model Checking
  • Modular Model Checking of Software Specifications with Simultaneous Environment Generation
  • Rabin Tree and Its Application to Group Key Distribution
  • Using Overlay Networks to Improve VoIP Reliability
  • Integrity-Enhanced Verification Scheme for Software-Intensive Organizations
  • RCGES: Retargetable Code Generation for Embedded Systems
  • Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri Nets
  • First-Order LTL Model Checking Using MDGs
  • Localizing Errors in Counterexample with Iteratively Witness Searching
  • Verification of WCDMA Protocols and Implementation
  • Efficient Representation of Algebraic Expressions
  • Development of RTOS for PLC Using Formal Methods
  • Reducing Parametric Automata: A Multimedia Protocol Service Case Study
  • Synthesis of State Feedback Controllers for Parameterized Discrete Event Systems
  • Solving Box-Pushing Games via Model Checking with Optimizations
  • CLP Based Static Property Checking
  • A Temporal Assertion Extension to Verilog.