Rajeev Alur (auth.), Farn Wang (eds.)3540236104, 9783540236108, 9783540304760
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.
Table of contents :
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 –
Reviews
There are no reviews yet.