快毕业了。毕业论文本来做的是非终止性增量式验证,但这种没有先例的题目还是太虚无缥缈了些,后来换成了上界分析。不过,准确地说应该是命令式程序中循环上界的验证,而不是生成。

论文的精简版本在这儿,需要自己编译(不会吧不会吧不会真的有人看我的论文吧):

linusboyle/bound-validate
Contribute to linusboyle/bound-validate development by creating an account on GitHub.

题目是「基于安全属性检查的程序上界验证方法」,要说技术含量,那基本上等于0,只不过包裹上形式化验证的皮,看上去偏理论一点而已。Safety Check就是个筐,什么问题都可以往里装,反正也不管可不可以判定,归约就完事儿了。但话又说回来,简单粗暴,倒也适合短平快地做毕设就是(笑)。