Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

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
  • © 2003

Overview

Editors:
  1. Daniel Geist

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

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Enrico Tronci

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

    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 2860)

Included in the following conference series:

Conference proceedings info: CHARME 2003.

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

Access this book

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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

Licence this eBook for your library

Institutional subscriptions

Keywords

Table of contents (35 papers)

  1. Front Matter

    Download chapter PDF

  2. Invited Talks

    1. What Is beyond the RTL Horizon for Microprocessor and System Design?

      • Wolfgang Roesner
      Pages 1-1

    2. The Charme of Abstract Entities

      • Fabio Somenzi
      Pages 2-2

  4. Software Verification

    1. Finding Regularity: Describing and Analysing Circuits That Are Not Quite Regular

      • Mary Sheeran
      Pages 4-18

    2. Predicate Abstraction with Minimum Predicates

      • Sagar Chaki, Edmund Clarke, Alex Groce, Ofer Strichman
      Pages 19-34

    3. Efficient Symbolic Model Checking of Software Using Partial Disjunctive Partitioning

      • Sharon Barner, Ishai Rabinovitz
      Pages 35-50

  5. 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. A Hazards-Based Correctness Statement for Pipelined Circuits

      • Mark D. Aagaard
      Pages 66-80

    3. Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT

      • Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind
      Pages 81-95

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

    3. “More Deterministic” vs. “Smaller” Büchi Automata for Efficient LTL Model Checking

      • Roberto Sebastiani, Stefano Tonetta
      Pages 126-140

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

  8. Specification Methods

    1. Reasoning about GSTE Assertion Graphs

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

    2. Towards Diagrammability and Efficiency in Event Sequence Languages

      • Kathi Fisler
      Pages 185-199

    3. Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving

      • Mike Gordon, Joe Hurd, Konrad Slind
      Pages 200-215
Back to top

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

Publish with us

Policies and ethics

Back to top

Search

Navigation