2004年第2届国际验证与分析的自动化技术会议录

2004年11月  

1 (2004年11月23日)  

Farn Wang  

504  

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格式下载