Correct hardware design and verification methods : 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 4 7, 2001 : proceedings
This volume contains the proceedings of CHARME 2001, the Eleventh Advanced Research Working Conference on Correct Hardware Design and Veri?cation Methods. CHARME 2001 is the 11th in a series of working conferences devoted to the development and use of leading-edge formal techniques and tools for the...
Enregistré dans:
| Institution som forfatter: | |
|---|---|
| Andre forfattere: | , |
| Format: | Livre numérique |
| Sprog: | Anglais |
| Udgivet: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Serier: | Lecture notes in computer science
2144 |
| Fag: | |
| Online adgang: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Kommentar: |
Archives Springer e-books (Licence nationale) Archives Springer e-books (Licence nationale) |
| Autres localisations: | Voir dans le Sudoc |
| Edition sous un autre format: | • Correct hardware design and verification methods, 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Livingston, Scotland, UK, September 4-7, 2001, proceedings, Tiziana Margaria, Tom Melham (eds.), 2001, New York, Springer, 1 vol. (XII-482 p.), Lecture notes in computer science, 3-540-42541-1 • Correct Hardware Design and Verification Methods, Texte imprimé, 9783662199329 |
Indholdsfortegnelse:
- Invited Contributions
- View from the Fringe of the Fringe
- Hardware Synthesis Using SAFL and Application to Processor Design
- FMCAD 2000
- Applications of Hierarchical Verification in Model Checking
- Model Checking 1
- Pruning Techniques for the SAT-Based Bounded Model Checking Problem
- Heuristics for Hierarchical Partitioning with Application to Model Checking
- Short Papers 1
- Efficient Reachability Analysis and Refinement Checking of Timed Automata Using BDDs
- Deriving Real-Time Programs from Duration Calculus Specifications
- Reproducing Synchronization Bugs with Model Checking
- Formally-Based Design Evaluation
- Clocking Issues
- Multiclock Esterel
- Register Transformations with Multiple Clock Domains
- Temporal Properties of Self-Timed Rings
- Short Papers 2
- Coverability Analysis Using Symbolic Model Checking
- Specifying Hardware Timing with ET-Lotos
- Formal Pipeline Design
- Verification of Basic Block Schedules Using RTL Transformations
- Joint Session with TPHOLs
- Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking
- Proof Engineering in the Large: Formal Verification of Pentium®4 Floating-Point Divider
- Hardware Compilation
- Towards Provably-Correct Hardware Compilation Tools Based on Pass Separation Techniques
- A Higher-Level Language for Hardware Synthesis
- Tools
- Hierarchical Verification Using an MDG-HOL Hybrid Tool
- Exploiting Transition Locality in Automatic Verification
- Efficient Debugging in a Formal Verification Environment
- Model Checking 2
- Using Combinatorial Optimization Methods for Quantification Scheduling
- Net Reductions for LTL Model-Checking
- Component Verification
- Formal Verification of the VAMP Floating Point Unit
- A Specification Methodology by a Collection ofCompact Properties as Applied to the Intel® Itanium Processor Bus Protocol
- The Design and Verification of a Sorter Core
- Case Studies
- Refinement-Based Formal Verification of Asynchronous Wrappers for Independently Clocked Domains in Systems on Chip
- Using Abstract Specifications to Verify PowerPC Custom Memories by Symbolic Trajectory Evaluation
- Algorithm Verification
- Formal Verification of Conflict Detection Algorithms
- Induction-Oriented Formal Verification in Symmetric Interconnection Networks
- A Framework for Microprocessor Correctness Statements
- Duration Calculus
- From Operational Semantics to Denotational Semantics for Verilog
- Efficient Verification of a Class of Linear Hybrid Automata Using Linear Programming.