高阶程序时间安全性的抽象解释

《Proceedings of the ACM on Programming Languages》：Abstract Interpretation of Temporal Safety Effects of Higher Order Programs

本文提出一种基于抽象解释的新方法，用于验证递归高阶程序的时间安全性属性。通过引入自动机抽象域和转换器，有效提升了大规模程序的验证效率和准确性，并对比了现有工具的性能。

　　

摘要

本文提出了一种基于抽象解释的新方法，用于验证递归高阶程序的时间安全属性。尽管之前的研究在理论层面取得了进展并实现了一定程度的自动化，但它们的可扩展性有限。我们首先引入了一种新的基于自动机的“抽象效应域”，用于概括上下文敏感的依赖效应，该领域能够抽象程序环境与自动机控制状态之间的关系。我们的分析还包括一种新的转换器，用于将事件前缀抽象为自动计算出的上下文敏感的效应摘要，并将其应用于基于抽象解释的类型-效应系统中。由于该分析依赖于自动机的参数设置，我们进一步将其扩展到更广泛的历史/注册（或“累积器”）自动机类别，从而能够表达一些无上下文依赖的属性，如输入依赖性、事件求和、资源使用情况、成本、事件幅度等。我们实现了一个名为evDrift的原型，它可以计算类似OCaml的递归高阶程序的依赖效应摘要（并验证断言）。作为对比，我们还描述了将这种方法简化为对无效应的高阶程序进行断言检查的方法，并证明了我们的方法在性能上优于之前的工具Drift、RCaml/Spacer、MoCHi和ReTHFL。在23个基准测试中，Drift验证了12个基准测试，RCaml/Spacer验证了6个，MoCHi验证了11个，ReTHFL验证了18个，而evDrift在这些工具都能解决的基准测试中分别实现了6.3倍、5.3倍、16.8倍和6.4倍的加速效果。