Correct Hardware Design and Verification Methods

Inhaltsverzeichnis

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