Accession Number : ADA288583

Title :   Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking.

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Personal Author(s) : Clarke, E. ; Grumberg, O. ; McMillan, K. ; Zhao, X.

PDF Url : ADA288583

Report Date : OCT 1994

Pagination or Media Count : 20

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.

Descriptors :   *COMPUTER AIDED DESIGN, *COMPUTER LOGIC, *CIRCUIT TESTERS, ALGORITHMS, VERIFICATION, EFFICIENCY, CONTAINMENT(GENERAL), SEQUENCES, SEARCHING, LANGUAGE, CIRCUITS, AUTOMATIC.

Subject Categories : Computer Programming and Software
      Electrical and Electronic Equipment

Distribution Statement : APPROVED FOR PUBLIC RELEASE