Correct Hardware Design and Verification Methods

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.