期刊文献+
共找到2篇文章
< 1 >
每页显示 20 50 100
VASR-CBMC:基于变量子图的多线程程序验证
1
作者 李运筹 尹平 尹良泽 《计算机应用研究》 CSCD 北大核心 2018年第8期2393-2396,共4页
Yogar-CBMC基于事件顺序图实现了反例抽象精化思想,是当前最有效的多线程程序验证工具之一。针对事件顺序图过于复杂,导致判断反例可行性及求解精化约束耗时过长的问题,提出变量子图概念及基于变量子图的抽象精化方法,将全局事件顺序图... Yogar-CBMC基于事件顺序图实现了反例抽象精化思想,是当前最有效的多线程程序验证工具之一。针对事件顺序图过于复杂,导致判断反例可行性及求解精化约束耗时过长的问题,提出变量子图概念及基于变量子图的抽象精化方法,将全局事件顺序图分解为连通等价的变量子图集,基于变量子图执行反例验证与精化求解,从而有效缩小图的规模,提升验证效率。将该方法实现为VSAR-CBMC,实验证明其相较于Yogar-CBMC验证时间平均缩短43%,有效提升了模型检验对并发程序的验证能力。 展开更多
关键词 程序验证 变量子图 反例抽象精化 事件顺序
下载PDF
Blind and readable image watermarking using wavelet tree quantization
2
作者 HUYuping YUShengsheng ZHOUJingLi SHILei 《Journal of Chongqing University》 CAS 2004年第1期34-38,共5页
A blind and readable image watermarking scheme using wavelet tree quantization is proposed. In order to increase the algorithm robustness and ensure the watermark integrity,error correction coding techniques are used ... A blind and readable image watermarking scheme using wavelet tree quantization is proposed. In order to increase the algorithm robustness and ensure the watermark integrity,error correction coding techniques are used to encode the embedded watermark. In the watermark embedding process, the wavelet coefficients of the host image are grouped into wavelet trees and each watermark bit is embedded by using two trees. The trees are so quantized that they exhibit a large enough statistical difference, which will later be used for watermark extraction. The experimental results show that the proposed algorithm is effective and robust to common image processing operations and some geometric operations such as JPEG compression, JPEG2000 compression, filtering, Gaussian noise attack, and row-column removal. It is demonstrated that the proposed technique is practical. 展开更多
关键词 readable image watermrk error correction code wavelet transform QUANTIZATION
下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部