TY  - BOOK
AU  - Wang,Farn
ED  - SpringerLink (Online service)
TI  - Automated Technology for Verification and Analysis: Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31-November 3, 2004. Proceedings 
T2  - Lecture Notes in Computer Science,
SN  - 9783540304760
AV  - QA76.9.L63 
U1  - 005.1015113 23
PY  - 2004///
CY  - Berlin, Heidelberg
PB  - Springer Berlin Heidelberg
KW  - Computer science
KW  - Computer Communication Networks
KW  - Software engineering
KW  - Logic design
KW  - Information systems
KW  - Computer Science
KW  - Logics and Meanings of Programs
KW  - Information Systems and Communication Service
KW  - Special Purpose and Application-Based Systems
KW  - Software Engineering
KW  - Programming Languages, Compilers, Interpreters
N1  - 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
UR  - http://dx.doi.org/10.1007/b102065
ER  -