Automated technology for verification and analysis : second international conference, ATVA 2004, Taipei, Taiwan, ROC, october 31-november 3, 2004 : proceedings
Enregistré dans:
| Collectivité auteur: | |
|---|---|
| Autres auteurs: | |
| Format: | Livre numérique |
| Langue: | Anglais |
| Publié: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Collection: | Lecture notes in computer science
3299 |
| Sujets: | |
| Accès en ligne: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Note: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Automated technology for verification and analysis, second international conference, ATVA 2004, Taipei, Taiwan, ROC, october 31-november 3, 2004, proceedings, Farn Wang (ed.), Berlin, Springer, 2004, 1 vol. (XII-506 p.), Lecture notes in computer science, 3-540-23610-4 • Automated Technology for Verification and Analysis, Texte imprimé, 9783662191248 |
Table des matières:
- 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
- MutationCoverage 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.