多面体抽象域的正确性证书的高效生成
编程语言
2013-04-04 v1 计算机科学中的逻辑
数学软件
摘要
多面体是使用抽象解释推断程序运行时属性的一个成熟抽象域。为了整个静态分析结果可信，需要对多面体上的计算进行认证。在这项工作中，我们探讨了在后验验证的道路上能走多远，以降低多面体抽象域认证的开销。我们展示了使包含证书生成成本可忽略的方法。从性能角度来看，我们基于单一表示、约束的实现与最先进的实现相当。
引用
@article{arxiv.1304.0864,
title = {Efficient Generation of Correctness Certificates for the Abstract Domain of Polyhedra},
author = {Alexis Fouilhé and David Monniaux and Michaël Périn},
journal= {arXiv preprint arXiv:1304.0864},
year = {2013}
}