开发者社区

文档建议反馈控制台

文章/答案/技术大牛

发布

社区首页 >问答首页 >z3 smt示例mini_ic3.py

问z3 smt示例mini_ic3.py
EN

Stack Overflow用户

提问于 2019-06-19 10:58:16

回答 1查看 59关注 0票数 1

我已经下载了z3并找到了一个mini_ic3.py程序？我认为它适用于ic3--一个归纳不变的-based形式验证程序。

要理解z3目录中的mini_ic3.py，有没有值得推荐的参考文献

EN

回答 1

Stack Overflow用户

发布于 2019-06-19 15:12:35

恐怕没有太多直接描述特定实现的内容。最好的办法是通读https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-bounded-model-checking

最初的IC3论文本身也会有所帮助。下面是一个很棒的介绍：http://theory.stanford.edu/~arbrad/papers/Understanding_IC3.pdf

票数 1

EN

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/56659443

复制

相似问题