Computer Science Department
School of Computer Science, Carnegie Mellon University
Convergence Testing in Term-Level
Bounded Model Checking
Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia
A shorter version of this paper will appear at CHARME '03.
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.