file.pdf (249.26 kB)
0/0

Convergence Testing in Term-Level Bounded Model Checking

Download (249.26 kB)
journal contribution
posted on 01.01.1983 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.

History

Publisher Statement

All Rights Reserved

Date

01/01/1983

Exports

Exports