Smallfoot 中的验证条件生成与变量条件
计算机科学中的逻辑
2012-04-24 v1 编程语言
摘要
这些笔记是文献 [1] 的 companion，描述了：Smallfoot 检查的变量条件、用于检查这些条件的分析、用于计算对应于带注释程序的验证条件集的算法，以及对并发资源初始化代码的处理。
引用
@article{arxiv.1204.4804,
title = {Verification Condition Generation and Variable Conditions in Smallfoot},
author = {Josh Berdine and Cristiano Calcagno and Peter W. O'Hearn},
journal= {arXiv preprint arXiv:1204.4804},
year = {2012}
}