《2004年第2届国际验证与分析的自动化技术会议录（计算机科学学术讲座纪要 卷3299）Automated Technology for Verification and Analysis》亚马逊编辑推荐：
在线阅读本书
This book constitutes the refereed proceedings of the Second International Conference on Automated Technology for Verificaton and Analysis, ATVA 2004, held in Taipei, Taiwan in October/November 2004. The 24 revised full papers presented together with abstracts of 6 invited presentations and 7 special track papers were carefully reviewed and selected from 69 submissions. Among the topics addressed are model-checking theory, theorem-proving theory, state-space reduction techniques, languages in automated verification, parametric analysis, optimization, formal performance analysis, real-time systems, embedded systems, infinite-state systems, Petri nets, UML, synthesis, and tools.
《2004年第2届国际验证与分析的自动化技术会议录（计算机科学学术讲座纪要 卷3299）Automated Technology for Verification and Analysis》内容简介 ：
The LNCS series reports state-of-the-art restilts in computer science research, development, and education, at a high lewl and in both printed and electronic form. Enjoying tight cooperation with the R&D community, with numerous individuals, as wetl as with prestigious organizations and
societies, LNCS has grown into the most comprehensiye computer science research forum available.
The scope of LNCS, including its subseries LNAI and LNBI, spans the whole range 0f computer science ard information technology including interdisciplinary topics in a vatety of application fields. The type of materia! published traditionatly includes
-proceedings-(published:in time for the lrespective conference)
-post-proceedings (consisting of thorodghly revised final full papers)
-research monographs (which may be based on outstanding PhD work,research projects, technical reports, etc.)
当当目录 ：
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
Biichi 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
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 (The Electronic Throttle Control Case Study)
Providing Automated Verification in HOL Using MDGs
Specification, Abduction, and Proof
Introducing Structural Dynamic Changes in Petri Nets Marked-Controlled Reconfigurable Nets
……
Author Index