Convergence Testing in Term-Level Bounded Model Checking
Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia · 2003
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 semidecision procedure to check this criterion based on a translation to quantified separation logic.Preliminary results on simple pipeline processor models are presented.