2004年第2屆國際驗證與分析的自動化技術會議錄

內容概要

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 andsocieties, 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 RefinementInvited Speech  Tools for Automated Verification of Web Services  Theorem Proving Languages for Verification  An Automated Rigorous Review Method for Verifying and Validating Formal SpecificationsPapers  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

圖書封面

評論、評分、閱讀與下載

---

    2004年第2屆國際驗證與分析的自動化技術會議錄 PDF格式下載

---