Approximate Symbolic Model Checking Using Overlapping Projections

Abstract

Abstract Symbolic Model Checking extends the scope of verification algorithms that can be handled automatically, by using symbolic representations rather than explicitly searching the entire state space of the model. However even the most sophisticated symbolic methods cannot be directly applied to many of today's large designs because of the state explosion problem. Approximate symbolic model checking is an attempt to trade off accuracy with the capacity to deal with bigger designs. This paper explores the idea of using overlapping projections as the underlying approximation scheme. The idea is evaluated by applying it to several modules from the I/O unit in the Stanford FLASH Multiprocessor, and some larger circuits in ISCAS89 benchmark suite.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1999
Accession Number
ADA401014

Entities

People

  • David L. Dill
  • Shankar G. Govindaraju

Organizations

  • Stanford University

Tags

Communities of Interest

  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Boundaries
  • Buildings And Structures
  • Computations
  • Computer Programming
  • Computers
  • Construction
  • Contrast
  • Demographic Cohorts
  • Errors
  • High Density
  • Iterations
  • Multiprocessors
  • Numbers
  • Real Numbers
  • Verification

Fields of Study

  • Computer science

Readers

  • Artificial Intelligence
  • Mathematical Modeling and Probability Theory.
  • Parallel and Distributed Computing.

Technology Areas

  • Space