【发布时间】：2019-11-01 16:59:27
【问题描述】：
我已经下载了z3并找到了一个mini_ic3.py程序？我认为它适用于 ic3——一个基于归纳不变式的形式验证程序。
是否有一些参考论文可以推荐用于理解 z3 目录中的 mini_ic3.py
【问题讨论】：
【发布时间】：2019-11-01 16:59:27
【问题描述】：
恐怕没有太多直接描述该特定实现。最好的办法是通读https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-bounded-model-checking
最初的 IC3 论文本身也会有所帮助。以下是精彩介绍：http://theory.stanford.edu/~arbrad/papers/Understanding_IC3.pdf
【讨论】：