Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking.

Abstract

Model checking is an automatic technique for verifying sequential circuit designs and protocols. An efficient search procedure is used to determine whether or not the specification is satisfied. If it is not satisfied, our technique will produce a counterexample execution trace that shows the cause of the problem. Although finding counterexamples is extremely important, there is no description of how to do this in the literature on model checking. We describe an efficient algorithm to produce counterexamples and witnesses for symbolic model checking algorithms. This algorithm is used in the SMV model checker and works quite well in practice. We also discuss how to extend our technique to more complicated specifications. This extension makes it possible to find counterexamples for verification procedures based on showing language containment between various types of w-automata.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1994
Accession Number
ADA288583

Entities

People

  • E. Clarke
  • K. Mcmillan
  • O. Grumberg
  • Xingchen Zhao

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Human Systems

DTIC Thesaurus Topics

  • Air Force
  • Algorithms
  • Alphabets
  • Automata
  • Computations
  • Computer Science
  • Computers
  • Finite Alphabet
  • Governments
  • Language
  • Notation
  • Sequences
  • Specifications
  • Standards
  • Transitions
  • United States
  • Verification

Fields of Study

  • Computer science

Readers

  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Mathematical Modeling and Probability Theory.