Finite differencing of logical formulas for static analysis
Finite differencing of logical formulas for static analysis
复制标题
静态分析逻辑公式的有限差分
DOI：
10.1145/1749608.1749613
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Alexey Loginov
中科院分区：
文献类型：
--
作者：
T. Reps;Shmuel Sagiv;Alexey Loginov
本文涉及维持仪器关系价值（也称为派生的关系或视图）的机制，该机制是通过逻辑公式而不是核心关系定义的，这是响应核心关系值的变化而定义的。它提出了一种将仪器关系的定义公式转换为关系维护公式的算法，该公式捕获了仪器关系的新价值。该算法以定义公式的大小在时间线性上运行。
该技术适用于程序分析问题，其中使用逻辑公式来表达语句的语义，以描述对核心关系值的变化。它提供了一种获取仪器关系值的方法，以反映通过执行给定语句产生的核心关系值的变化。
我们提供了实验证据，表明我们的技术是一种有效的证据：对于各种基准，使用我们的方法自动生产的关系维护公式产生的精度与最佳可用手工制作的公式相同。
This article concerns mechanisms for maintaining the value of an instrumentation relation (also known as a derived relation or view), defined via a logical formula over core relations, in response to changes in the values of the core relations. It presents an algorithm for transforming the instrumentation relation's defining formula into a relation-maintenance formula that captures what the instrumentation relation's new value should be. The algorithm runs in time linear in the size of the defining formula.
The technique applies to program analysis problems in which the semantics of statements is expressed using logical formulas that describe changes to core relation values. It provides a way to obtain values of the instrumentation relations that reflect the changes in core relation values produced by executing a given statement.
We present experimental evidence that our technique is an effective one: for a variety of benchmarks, the relation-maintenance formulas produced automatically using our approach yield the same precision as the best available hand-crafted ones.