论文标题
编译器优化验证框架的差异测试（经验论文）
Differential Testing of a Verification Framework for Compiler Optimizations (Experience Paper)
论文作者
论文摘要
我们要验证GRAALVM编译器中优化阶段的正确性，该阶段由数千行的复杂Java代码组成，它们执行复杂的图形转换。我们已经使用isabelle/hol定理供奉献者建立了代码数据结构和操作的高级模型，并可以正式验证这些高级操作的正确性。但是剩下的挑战是：我们如何确定那些高级操作准确地反映了Java在做什么？本文通过应用几种不同类型的差分测试来验证正式模型和Java代码具有相同的语义来解决该问题。这些验证技术中的许多应适用于其他正在构建现实代码正式模型的项目。
We want to verify the correctness of optimization phases in the GraalVM compiler, which consist of many thousands of lines of complex Java code performing sophisticated graph transformations. We have built high-level models of the data structures and operations of the code using the Isabelle/HOL theorem prover, and can formally verify the correctness of those high-level operations. But the remaining challenge is: how can we be sure that those high-level operations accurately reflect what the Java is doing? This paper addresses that issue by applying several different kinds of differential testing to validate that the formal model and the Java code have the same semantics. Many of these validation techniques should be applicable to other projects that are building formal models of real-world code.
