We study partial quantifier elimination (PQE) for propositional CNF formulas with existential quantifiers. PQE is a generalization of quantifier elimination where one can limit the set of clauses taken out of the scope of quantifiers to a small subset of clauses. The appeal of PQE is that many verification problems (e.g. equivalence checking and model checking) can be solved in terms of PQE and the latter can be dramatically simpler than full quantifier elimination. We show that PQE can be used for property generation that can be viewed as a generalization of testing. The objective here is to produce an $\mathit{unwanted}$ property of a design implementation thus exposing a bug. We introduce two PQE solvers called $\mathit{EG}$-$\mathit{PQE}$ and $\mathit{EG}$-$\mathit{PQE}^+$. $\mathit{EG}$-$\mathit{PQE}$ is a very simple SAT-based algorithm. $\mathit{EG}$-$\mathit{PQE}^+$ is more sophisticated and robust than $\mathit{EG}$-$\mathit{PQE}$. We use these PQE solvers to find an unwanted property (namely, an unwanted invariant) of a buggy FIFO buffer. We also apply them to invariant generation for sequential circuits from a HWMCC benchmark set. Finally, we use these solvers to generate properties of a combinational circuit that mimic symbolic simulation.


翻译:暂无翻译

0
下载
关闭预览

相关内容

Eurographics是唯一在欧洲范围内真正的专业计算机图形协会。它汇集了来自世界各地的图形专家,该协会支持其成员推进计算机图形学以及多媒体,科学可视化和人机界面等相关领域的最新技术水平。通过其全球成员资格,EG与美国,日本和其他国家/地区的发展保持着密切联系,从而促进了全球范围内科学技术信息和技能的交流。 官网地址:http://dblp.uni-trier.de/db/conf/eurographics/
不可错过!《机器学习100讲》课程,UBC Mark Schmidt讲授
专知会员服务
73+阅读 · 2022年6月28日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
78+阅读 · 2020年7月26日
专知会员服务
60+阅读 · 2020年3月19日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
28+阅读 · 2019年5月18日
深度自进化聚类:Deep Self-Evolution Clustering
我爱读PAMI
15+阅读 · 2019年4月13日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
vae 相关论文 表示学习 1
CreateAMind
12+阅读 · 2018年9月6日
Capsule Networks解析
机器学习研究会
11+阅读 · 2017年11月12日
【推荐】YOLO实时目标检测(6fps)
机器学习研究会
20+阅读 · 2017年11月5日
【推荐】GAN架构入门综述(资源汇总)
机器学习研究会
10+阅读 · 2017年9月3日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Arxiv
0+阅读 · 2023年7月13日
Arxiv
0+阅读 · 2023年7月8日
VIP会员
相关VIP内容
不可错过!《机器学习100讲》课程,UBC Mark Schmidt讲授
专知会员服务
73+阅读 · 2022年6月28日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
78+阅读 · 2020年7月26日
专知会员服务
60+阅读 · 2020年3月19日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
机器学习入门的经验与建议
专知会员服务
92+阅读 · 2019年10月10日
【哈佛大学商学院课程Fall 2019】机器学习可解释性
专知会员服务
103+阅读 · 2019年10月9日
相关资讯
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
28+阅读 · 2019年5月18日
深度自进化聚类:Deep Self-Evolution Clustering
我爱读PAMI
15+阅读 · 2019年4月13日
Unsupervised Learning via Meta-Learning
CreateAMind
42+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
vae 相关论文 表示学习 1
CreateAMind
12+阅读 · 2018年9月6日
Capsule Networks解析
机器学习研究会
11+阅读 · 2017年11月12日
【推荐】YOLO实时目标检测(6fps)
机器学习研究会
20+阅读 · 2017年11月5日
【推荐】GAN架构入门综述(资源汇总)
机器学习研究会
10+阅读 · 2017年9月3日
相关基金
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2013年12月31日
国家自然科学基金
1+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2009年12月31日
Top
微信扫码咨询专知VIP会员