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.
Author(s): Rajeev Alur (auth.), Farn Wang (eds.)
Series: Lecture Notes in Computer Science 3299
Edition: 1
Publisher: Springer-Verlag Berlin Heidelberg
Year: 2004
Language: English
Pages: 510
Tags: Logics and Meanings of Programs; Information Systems and Communication Service; Computer Communication Networks; Special Purpose and Application-Based Systems; Software Engineering; Programming Languages, Compilers, Interpreters
Front Matter....Pages -
Games for Formal Design and Verification of Reactive Systems....Pages 1-1
Evolution of Model Checking into the EDA Industry....Pages 2-6
Abstraction Refinement....Pages 7-7
Tools for Automated Verification of Web Services....Pages 8-10
Theorem Proving Languages for Verification....Pages 11-14
An Automated Rigorous Review Method for Verifying and Validating Formal Specifications....Pages 15-19
Toward Unbounded Model Checking for Region Automata....Pages 20-33
Search Space Partition and Case Basis Exploration for Reducing Model Checking Complexity....Pages 34-48
Synthesising Attacks on Cryptographic Protocols....Pages 49-63
Büchi Complementation Made Tighter....Pages 64-78
SAT-Based Verification of Safe Petri Nets....Pages 79-92
Disjunctive Invariants for Numerical Systems....Pages 93-107
Validity Checking for Quantifier-Free First-Order Logic with Equality Using Substitution of Boolean Formulas....Pages 108-119
Fair Testing Revisited: A Process-Algebraic Characterisation of Conflicts....Pages 120-134
Exploiting Symmetries for Testing Equivalence in the Spi Calculus....Pages 135-149
Using Block-Local Atomicity to Detect Stale-Value Concurrency Errors....Pages 150-164
Abstraction-Based Model Checking Using Heuristical Refinement....Pages 165-178
A Global Timed Bisimulation Preserving Abstraction for Parametric Time-Interval Automata....Pages 179-195
Design and Evaluation of a Symbolic and Abstraction-Based Model Checker....Pages 196-210
Component-Wise Instruction-Cache Behavior Prediction....Pages 211-229
Validating the Translation of an Industrial Optimizing Compiler....Pages 230-247
Composition of Accelerations to Verify Infinite Heterogeneous Systems....Pages 248-262
Hybrid System Verification Is Not a Sinecure....Pages 263-277
Providing Automated Verification in HOL Using MDGs....Pages 278-293
Specification, Abduction, and Proof....Pages 294-309
Introducing Structural Dynamic Changes in Petri Nets: Marked-Controlled Reconfigurable Nets....Pages 310-323
Typeness for ω -Regular Automata....Pages 324-338
Partial Order Reduction for Detecting Safety and Timing Failures of Timed Circuits....Pages 339-353
Mutation Coverage Estimation for Model Checking....Pages 354-368
Modular Model Checking of Software Specifications with Simultaneous Environment Generation....Pages 369-383
Rabin Tree and Its Application to Group Key Distribution....Pages 384-391
Using Overlay Networks to Improve VoIP Reliability....Pages 392-401
Integrity-Enhanced Verification Scheme for Software-Intensive Organizations....Pages 402-414
RCGES: Retargetable Code Generation for Embedded Systems....Pages 415-425
Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri Nets....Pages 426-440
First-Order LTL Model Checking Using MDGs....Pages 441-455
Localizing Errors in Counterexample with Iteratively Witness Searching....Pages 456-469
Verification of WCDMA Protocols and Implementation....Pages 470-473
Efficient Representation of Algebraic Expressions....Pages 474-478
Development of RTOS for PLC Using Formal Methods....Pages 479-482
Reducing Parametric Automata: A Multimedia Protocol Service Case Study....Pages 483-486
Synthesis of State Feedback Controllers for Parameterized Discrete Event Systems....Pages 487-490
Solving Box-Pushing Games via Model Checking with Optimizations....Pages 491-494
CLP Based Static Property Checking....Pages 495-498
A Temporal Assertion Extension to Verilog....Pages 499-504
Back Matter....Pages -
