Skip to main content
  • Conference proceedings
  • © 2003

Correct Hardware Design and Verification Methods

12th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2003, L'Aquila, Italy, October 21-24, 2003, Proceedings

Conference proceedings info: CHARME 2003.

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

This is a preview of subscription content, log in via an institution to check for access.

Table of contents (35 papers)

  1. Front Matter

  2. Invited Talks

    1. The Charme of Abstract Entities

      • Fabio Somenzi
      Pages 2-2
  3. Software Verification

    1. Predicate Abstraction with Minimum Predicates

      • Sagar Chaki, Edmund Clarke, Alex Groce, Ofer Strichman
      Pages 19-34
  4. Processor Verification

    1. Instantiating Uninterpreted Functional Units and Memory System: Functional Verification of the VAMP

      • Sven Beyer, Chris Jacobi, Daniel Kröning, Dirk Leinenbach, Wolfgang J. Paul
      Pages 51-65
    2. Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT

      • Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind
      Pages 81-95
  5. Automata Based Methods

    1. On Complementing Nondeterministic Büchi Automata

      • Sankar Gurumurthy, Orna Kupferman, Fabio Somenzi, Moshe Y. Vardi
      Pages 96-110
    2. Coverage Metrics for Formal Verification

      • Hana Chockler, Orna Kupferman, Moshe Y. Vardi
      Pages 111-125
  6. Short Papers 1

    1. An Optimized Symbolic Bounded Model Checking Engine

      • Rachel Tzoref, Mark Matusevich, Eli Berger, Ilan Beer
      Pages 141-149
    2. Constrained Symbolic Simulation with Mathematica and ACL2

      • Ghiath Al Sammane, Diana Toma, Julien Schmaltz, Pierre Ostier, Dominique Borrione
      Pages 150-157
    3. Semi-formal Verification of Memory Systems by Symbolic Simulation

      • Husam Abu-Haimed, Sergey Berezin, David L. Dill
      Pages 158-163
    4. CTL May Be Ambiguous When Model Checking Moore Machines

      • Cédric Roux, Emmanuelle Encrenaz
      Pages 164-169
  7. Specification Methods

    1. Reasoning about GSTE Assertion Graphs

      • Alan J. Hu, Jeremy Casas, Jin Yang
      Pages 170-184

Other Volumes

  1. Correct Hardware Design and Verification Methods

Editors and Affiliations

  • IBM Haifa Research Lab., Haifa University, Mount Carmel Haifa, Israel

    Daniel Geist

  • Dipartimento di Informatica, Università di Roma “La Sapienza”, Roma, Italy

    Enrico Tronci

Bibliographic Information

Buy it now

Buying options

eBook USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access