快毕业了。毕业论文本来做的是非终止性增量式验证，但这种没有先例的题目还是太虚无缥缈了些，后来换成了上界分析。不过，准确地说应该是命令式程序中循环上界的验证，而不是生成。
论文的精简版本在这儿，需要自己编译（不会吧不会吧不会真的有人看我的论文吧）。
题目是「基于安全属性检查的程序上界验证方法」，要说技术含量，那基本上等于0，只不过包裹上形式化验证的皮，看上去偏理论一点而已。Safety Check就是个筐，什么问题都可以往里装，反正也不管可不可以判定，归约就完事儿了。但话又说回来，简单粗暴，倒也适合短平快地做毕设就是（笑）。
