Challenges in System-Level Design -- Generating Fast Multipliers Using Clever Circuits -- Verification of Analog and Mixed-Signal Circuits Using Hybrid System Techniques -- A Methodology for the Formal Verification of FFT Algorithms in HOL -- A Functional Approach to the Formal Specification of Networks on Chip -- Proof Styles in Operational Semantics -- Integrating Reasoning About Ordinal Arithmetic into ACL2 -- Combining Equivalence Verification and Completion Functions -- Synchronization-at-Retirement for Pipeline Verification -- Late Design Changes (ECOs) for Sequentially Optimized Esterel Designs -- Non-miter-based Combinational Equivalence Checking by Comparing BDDs with Different Variable Orders -- Scalable Automated Verification via Expert-System Guided Transformations -- Simple Yet Efficient Improvements of SAT Based Bounded Model Checking -- Simple Bounded LTL Model Checking -- QuBE++: An Efficient QBF Solver -- Bounded Probabilistic Model Checking with the Mur? Verifier -- Increasing the Robustness of Bounded Model Checking by Computing Lower Bounds on the Reachable States -- Bounded Verification of Past LTL -- A Hybrid of Counterexample-Based and Proof-Based Abstraction -- Memory Efficient All-Solutions SAT Solver and Its Application for Reachability Analysis -- Approximate Symbolic Model Checking for Incomplete Designs -- Extending Extended Vacuity -- Parameterized Vacuity -- An Operational Semantics for Weak PSL -- Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-Checking -- Bloom Filters in Probabilistic Verification -- A Simple Method for Parameterized Verification of Cache Coherence Protocols -- A Partitioning Methodology for BDD-Based Verification -- Invariant Checking Combining Forward and Backward Traversal -- Variable Reuse for Efficient Image Computation.