SymInfer：利用符号状态推断程序不变式
软件工程
2019-03-29 v1
摘要
我们提出了一种利用符号执行生成的符号状态来推断程序不变式的新技术。符号状态由路径条件和局部变量约束组成，是对具体程序状态集合的紧凑描述，可用于不变式推断与不变式验证。我们的技术采用一种基于反例的算法，该算法从符号状态创建具体状态，从具体状态推断候选不变式，然后使用符号状态验证或反驳候选不变式。在反驳情形下会产生具体反例，这些反例可防止虚假结果并使得该技术能获得更精确的不变式。当算法达到稳定的不变式集合时，该过程停止。我们介绍了 SymInfer，这是一个实现上述思想以在 Java 程序中任意位置自动生成不变式的工具。该工具从 Symbolic PathFinder 获取符号状态，并使用现有算法推断复杂（可能非线性的）数值不变式。我们的初步结果表明，SymInfer 能有效利用符号状态生成精确且有用的不变式，用于证明程序安全性和分析程序运行时复杂度。我们还表明 SymInfer 优于现有的不变式生成系统。
引用
@article{arxiv.1903.11768,
title = {SymInfer: Inferring Program Invariants using Symbolic States},
author = {ThanhVu Nguyen and Matthew B. Dwyer and Willem Visser},
journal= {arXiv preprint arXiv:1903.11768},
year = {2019}
}