CMU-CS-03-156
Computer Science Department
School of Computer Science, Carnegie Mellon University


CMU-CS-03-156

Convergence Testing in Term-Level
Bounded Model Checking

Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia

June 2003

A shorter version of this paper will appear at CHARME '03.

CMU-CS-03-156.ps (Unavailable)
CMU-CS-03-156.pdf


Keywords: Term-level verification, convergence in model checking, symbolic simulation, uninterpreted functions, second-order logic, decision procedures, quantified separation logic, processor verification


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 semi-decision procedures to check this criterion that are based on translations to quantified separation logic. Preliminary results on simple pipeline processor models are presented to demonstrate our approach.

21 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu