Convergence Testing in Term-Level Bounded Model Checking
Convergence Testing in Term-Level Bounded Model Checking
复制标题
项级有界模型检查中的收敛性测试
DOI：
10.1007/978-3-540-39724-3_31
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
S. Seshia
中科院分区：
文献类型：
--
作者：
R. Bryant;Shuvendu K. Lahiri;S. 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.