Automated Technology for Verification and Analysis Second International Conference, ATVA 2004, Taipei, Taiwan, ROC, October 31 - November 3, 2004. Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Wang, Farn (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 2004.
• Έκδοση: 1st ed. 2004.
• Σειρά: Lecture Notes in Computer Science, 3299
• Θέματα: Computer-aided engineering.; Computer logic.; Computers.; Computer communication systems.; Special purpose computers.; Software engineering.; Computer-Aided Engineering (CAD, CAE) and Design.; Logics and Meanings of Programs.; Information Systems and Communication Service.; Computer Communication Networks.; Special Purpose and Application-Based Systems.; Software Engineering.

Πίνακας περιεχομένων:

• 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
• Büchi 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 Errors
• 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
• Providing Automated Verification in HOL Using MDGs
• Specification, Abduction, and Proof
• Introducing Structural Dynamic Changes in Petri Nets: Marked-Controlled Reconfigurable Nets
• Typeness for ?-Regular Automata
• Partial Order Reduction for Detecting Safety and Timing Failures of Timed Circuits
• Mutation Coverage Estimation for Model Checking
• Modular Model Checking of Software Specifications with Simultaneous Environment Generation
• Rabin Tree and Its Application to Group Key Distribution
• Using Overlay Networks to Improve VoIP Reliability
• Integrity-Enhanced Verification Scheme for Software-Intensive Organizations
• RCGES: Retargetable Code Generation for Embedded Systems
• Verification of Analog and Mixed-Signal Circuits Using Timed Hybrid Petri Nets
• First-Order LTL Model Checking Using MDGs
• Localizing Errors in Counterexample with Iteratively Witness Searching
• Verification of WCDMA Protocols and Implementation
• Efficient Representation of Algebraic Expressions
• Development of RTOS for PLC Using Formal Methods
• Reducing Parametric Automata: A Multimedia Protocol Service Case Study
• Synthesis of State Feedback Controllers for Parameterized Discrete Event Systems
• Solving Box-Pushing Games via Model Checking with Optimizations
• CLP Based Static Property Checking
• A Temporal Assertion Extension to Verilog.