Accession Number:

ADA461050

Title:

Convergence Testing in Term-Level Bounded Model Checking

Descriptive Note:

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Report Date:

2003-06-01

Pagination or Media Count:

22.0

Abstract:

We consider the problem of bounded model checking of systems expressed in a decidable fragment of first-order logic. While model checking is not guaranteed to terminate for an arbitrary system, it converges for many practical examples, including pipelined processors. We give a new formal definition of convergence that generalizes previously stated criteria. We also give a sound semi-decision procedure to check this criterion based on a translation to quantified separation logic. Preliminary results on simple pipeline processor models are presented.

Subject Categories:

  • Computer Programming and Software
  • Computer Systems

Distribution Statement:

APPROVED FOR PUBLIC RELEASE