编译器优化验证框架的差分测试（经验论文）
计算机科学中的逻辑
2022-12-06 v1 编程语言
软件工程
摘要
我们希望验证 GraalVM 编译器中优化阶段的正确性，这些阶段由数千行执行复杂图变换的复杂 Java 代码组成。我们使用 Isabelle/HOL 定理证明器构建了代码数据结构与操作的高层模型，并能形式化验证这些高层操作的正确性。但剩余的挑战是：我们如何确信那些高层操作准确反映了 Java 代码的行为？本文通过应用若干不同种类的差分测试来验证形式化模型与 Java 代码具有相同的语义，从而解决该问题。许多此类验证技术应适用于其他正在构建现实代码形式化模型的项目。
引用
@article{arxiv.2212.01748,
title = {Differential Testing of a Verification Framework for Compiler Optimizations (Experience Paper)},
author = {Mark Utting and Brae J. Webb and Ian J. Hayes},
journal= {arXiv preprint arXiv:2212.01748},
year = {2022}
}
备注
8 pages, 6 figures