抽象解释的简洁表示
摘要：改进的静态分析技术和生成不相交不变量的技术的组合：路径及其符号表示和静态赋值的转换技术的捷径的技术所。 路径内的循环可以通过明确区分来提高抽象解释技术的准确性，但可能会导致指数级别的复杂度。通过SMT求解技术和路径及路径集合的稀疏表示，可以避免这个问题。为了确定某个抽象是否比其他抽象更准确，基于理论的局部准确性结果是困难的，因为抽象解释与扩大算子的结果不具有单调性。因此，我们在多个开源软件包上进行了广泛比较，以比较我们的新技术和之前的技术。
作者：Julien Henry (VERIMAG - IMAG), David Monniaux (VERIMAG - IMAG), Matthieu Moy (VERIMAG - IMAG)
论文ID：1206.4234
分类：Programming Languages
分类简称：cs.PL
提交时间：2012-06-20