file.pdf (249.26 kB)

Convergence Testing in Term-Level Bounded Model Checking

Download (249.26 kB)
journal contribution
posted on 01.01.1983, 00:00 by Randal E. Bryant, Shuvendu K. Lahiri, Sanjit A. Seshia
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.


Publisher Statement

All Rights Reserved