一句话：提出过程间推断所有有效双变量 Herbrand 等式的分析方法，并给出多项式时间不变式验证。
论文研究过程间 Herbrand 等式推断，针对所有赋值右侧至多依赖一个变量的程序，证明其全部有效 Herbrand 等式均可被过程间推断。方法基于过程摘要表示有限多个带模板变量通用后置条件的最弱前置条件；为有效表示这些前置条件，作者证明几乎全部运行时可能计算的值都可唯一分解为树模式与 ground term，并引入可判定的近似 subsumption，以保证有限等式合取不会无限增长。基于这些结果，论文实现有效不动点迭代，推断所有过程间有效的 Herbrand 等式，并进一步证明变量数恒定的不变候选可在多项式时间内验证。
We prove that all valid Herbrand equalities can be inter-procedurally inferred for programs where all assignments whose right-hand sides depend on at most one variable are taken into account. The analysis is based on procedure summaries representing the weakest pre-conditions for finitely many generic post-conditions with template variables. In order to arrive at effective representations for all occurring weakest pre-conditions, we show for almost all values possibly computed at run-time, that they can be uniquely factorized into tree patterns and a ground term. Moreover, we introduce an approximate notion of subsumption which is effectively decidable and ensures that finite conjunctions of equalities may not grow infinitely. Based on these technical results, we realize an effective fixpoint iteration to infer all inter-procedurally valid Herbrand equalities for these programs. Finally we show that an invariant candidate with a constant number of variables, can be verified in polynomial time.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{FrielinghausPS15,
title = {Inter-procedural Two-Variable Herbrand Equalities},
author = {Stefan Schulze Frielinghaus and Michael Petter and Helmut Seidl},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 2},
year = {2017},
doi = {10.23638/lmcs-13(2:5)2017}
}