Correct hardware design and verification methods : 10th IFIP WG10.5 advanced research working conference, CHARME'99, Bad Herrenalb, Germany, September 27-29, 1999 : proceedings
CHARME 99 is the tenth in a series of working conferences devoted to the dev- opment and use of leading-edge formal techniques and tools for the design and veri?cation of hardware and systems. Previous conferences have been held in Darmstadt (1984), Edinburgh (1985), Grenoble (1986), Glasgow (1988),...
Spremljeno u:
| Autor kompanije: | |
|---|---|
| Daljnji autori: | , |
| Format: | Livre numérique |
| Jezik: | Anglais |
| Izdano: |
Berlin [etc.] :
Springer
[20..].
Cham : Springer Nature |
| Serija: | Lecture notes in computer science
1703 |
| Teme: | |
| Online pristup: | Accès sur la plateforme de l'éditeur Accès sur la plateforme Istex Accès Université d'Orléans Accès INSA CVL |
| Bilješka: |
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, 10th IFIP WG10.5 advanced research working conference, CHARME'99, Bad Herrenalb, Germany, September 27-29, 1999, proceedings, Laurence Pierre, Thomas Kropf (eds.), 1999, Berlin, Springer, 1 vol. (XI-366 p.), Lecture notes in computer science, 3-540-66559-5 • Correct Hardware Design and Verification Methods, Texte imprimé, 9783662197691 |
Sadržaj:
- Invited Talks
- Esterel and Jazz : Two Synchronous Languages for Circuit Design
- Design Process of Embedded Automotive Systems Using Model Checking for Correct Specifications
- Proof of Microprocessors
- A Proof of Correctness of a Processor Implementing Tomasulo s Algorithm without a Reorder Buffer
- Formal Verification of Explicitly Parallel Microprocessors
- Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic
- Model Checking
- Model Checking TLA+ Specifications
- Efficient Decompositional Model Checking for Regular Timing Diagrams
- Vacuity Detection in Temporal Model Checking
- Formal Methods and Industrial Applications
- Using Symbolic Model Checking to Verify the Railway Stations of Hoorn-Kersenboogerd and Heerhugowaard
- Practical Application of Formal Verification Techniques on a Frame Mux/Demux Chip from Nortel Semiconductors
- Efficient Verification of Timed Automata Using Dense and Discrete Time Semantics
- Abstraction and Compositional Techniques
- From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking
- Automatic Error Correction of Large Circuits Using Boolean Decomposition and Abstraction
- Abstract BDDs: A Technique for Using Abstraction in Model Checking
- Theorem Proving Related Approaches
- Formal Synthesis at the Algorithmic Level
- Xs Are for Trajectory Evaluation, Booleans Are for Theorem Proving
- Verification of Infinite State Systems by Compositional Model Checking
- Symbolic Simulation/Symbolic Traversal
- Formal Verification of Designs with Complex Control by Symbolic Simulation
- Hints to Accelerate Symbolic Traversal
- Specification Languages and Methodologies
- Modeling and Checking Networks of CommunicatingReal-Time Processes
- Have I Written Enough Properties? - A Method of Comparison Between Specification and Implementation
- Program Slicing of Hardware Description Languages
- Posters
- Results of the Verification of a Complex Pipelined Machine Model
- Hazard Freedom Checking in Speed Independent Systems
- Yet Another Look at LTL Model Checking
- Verification of Finite-State-Machine Refinements Using a Symbolic Methodology
- Refinement and Property Checking in High-Level Synthesis Using Attribute Grammars
- A Systematic Incrementalization Technique and Its Application to Hardware Design
- Bisimulation and Model Checking
- Circular Compositional Reasoning about Liveness
- Symbolic Simulation of Microprocessor Models Using Type Classes in Haskell
- Exploiting Retiming in a Guided Simulation Based Validation Methodology
- Fault Models for Embedded Systems
- Validation of Object-Oriented Concurrent Designs by Model Checking.