Counterexample-guided Abstraction Refinement

Abstract

We present an automatic iterative abstraction-refinement methodology in which the initial abstract model is generated by an automatic analysis of the control structures in the program to be verified. Abstract models may admit erroneous (or "spurious" ) connterexamples. We devise new symbolic techniques which analyze such counterexamples and refine the abstract model correspondingly. The refinement algorithm keeps the size of the abstract state space small due to the use of abstraction functions which distinguish many degrees of abstraction for each program variable. We describe an implementation of our methodology in NuSMV. Practical experiments including a large Fujitsu IP core design with about 500 latches and 10000 lines of SMV code confirm the effectiveness of our approach.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2000
Accession Number
ADA374597

Entities

People

  • E. Clarke
  • H. Veith
  • O. Grumberg
  • Shalini Jha
  • Yao Lu

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Automatic
  • Coding
  • Computations
  • Computer Science
  • Computer-Aided Design
  • Concrete
  • Construction
  • Hardness
  • Language
  • Polynomials
  • Simulations
  • Specifications
  • Standards
  • Symbols
  • Transitions

Fields of Study

  • Computer science
  • Engineering
  • Geography

Readers

  • Computational Modeling and Simulation
  • Mathematical Modeling and Probability Theory.

Technology Areas

  • Space