Correct Hardware Design and Verification Methods 10th IFIP WG10.5 Advanced Research Working Conference, CHARME'99, Bad Herrenalb, Germany, September 27-29, 1999, Proceedings /

• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Άλλοι συγγραφείς: Pierre, Laurence (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt), Kropf, Thomas (Επιμελητής έκδοσης, http://id.loc.gov/vocabulary/relators/edt)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: Berlin, Heidelberg : Springer Berlin Heidelberg : Imprint: Springer, 1999.
• Έκδοση: 1st ed. 1999.
• Σειρά: Lecture Notes in Computer Science, 1703
• Θέματα: Architecture, Computer.; Computer engineering.; Computer hardware.; Computer logic.; Software engineering.; Computational complexity.; Computer System Implementation.; Computer Engineering.; Computer Hardware.; Logics and Meanings of Programs.; Software Engineering.; Complexity.

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 (1...

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

• 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 Communicating Real-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.