Correct hardware design and verification methods : 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L Aquila, Italy, October 21-24, 2003 : proceedings
Enregistré dans:
| 主要作者: | |
|---|---|
| 企业作者: | |
| 其他作者: | , |
| 格式: | Livre numérique |
| 语言: | Anglais |
| 出版: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| 丛编: | Lecture notes in computer science
2860 |
| 主题: | |
| 在线阅读: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| 提示: |
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, 12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, proceedings, Daniel Geist, Enrico Tronci, (Eds.), Berlin, Springer, 2003, 1 vol. (XII-426 p.), Lecture notes in computer science, 3-540-20363-X • Correct Hardware Design and Verification Methods, Texte imprimé, 9783662163191 |
书本目录:
- Invited Talks
- What Is beyond the RTL Horizon for Microprocessor and System Design?
- The Charme of Abstract Entities
- Tutorial
- The PSL/Sugar Specification Language A Language for all Seasons
- Software Verification
- Finding Regularity: Describing and Analysing Circuits That Are Not Quite Regular
- Predicate Abstraction with Minimum Predicates
- Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning
- Processor Verification
- Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP
- A Hazards-Based Correctness Statement for Pipelined Circuits
- Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT
- Automata Based Methods
- On Complementing Nondeterministic Büchi Automata
- Coverage Metrics for Formal Verification
- More Deterministic vs. Smaller Büchi Automata for Efficient LTL Model Checking
- Short Papers 1
- An Optimized Symbolic Bounded Model Checking Engine
- Constrained Symbolic Simulation with Mathematica and ACL2
- Semi-formal Verification of Memory Systems by Symbolic Simulation
- CTL May Be Ambiguous When Model Checking Moore Machines
- Specification Methods
- Reasoning about GSTE Assertion Graphs
- Towards Diagrammability and Efficiency in Event Sequence Languages
- Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving
- Protocol Verification
- On Combining Symmetry Reduction and Symbolic Representation for Efficient Model Checking
- On the Correctness of an Intrusion-Tolerant Group Communication Protocol
- Exact and Efficient Verification of Parameterized Cache Coherence Protocols
- Short Papers 2
- Design and Implementation of an Abstract Interpreter for VHDL
- A ProgrammingLanguage Based Analysis of Operand Forwarding
- Integrating RAM and Disk Based Verification within the Mur? Verifier
- Design and Verification of CoreConnectTM IP Using Esterel
- Theorem Proving
- Inductive Assertions and Operational Semantics
- A Compositional Theory of Refinement for Branching Time
- Linear and Nonlinear Arithmetic in ACL2
- Bounded Model Checking
- Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checking
- Convergence Testing in Term-Level Bounded Model Checking
- The ROBDD Size of Simple CNF Formulas
- Model Checking and Application
- Efficient Hybrid Reachability Analysis for Asynchronous Concurrent Systems
- Finite Horizon Analysis of Markov Chains with the Mur? Verifier
- Improved Symbolic Verification Using Partitioning Techniques.