%0 Journal Article
%T 变量极小不可满足在模型检测中的应用
%A 陈振宇？
%A 陶志红？
%A KLEINE
%A BüNING
%A Hans？
%A 王立福？
%J 软件学报
%P 39-47
%D 2008
%X 提出一个结合变量抽象和有界模型检测(bmc)的验证框架,用于证明反例不存在或输出存在反例.引入变量极小不可满足(vmu)的数学概念来驱动抽象精化的验证过程.一个vmu公式f的变量集合是保证其不可满足性的一个极小集合.严格证明了vmu驱动的精化满足抽象精化框架中的两个理想性质:有效性和极小性.虽然vmu的判定问题和极小不可满足(mu)一样难,即dp完全的,该案例研究表明,在变量抽象精化过程中,vmu比mu更为有效.
%K 极小不可满足
%K 抽象精化
%K 模型检测
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=20080105&flag=1