SHF: Small: VeriF-OPT, a Verification Framework for Optimizations and Program Transformations

现代世界依靠软件运行，而软件依靠编译器运行，这些程序弥合了人类可读的高级编程语言和计算机执行的低级机器代码之间的鸿沟。每年，数百万美元和无数小时的努力都用于确保软件的正确性和可靠性。然而，这种分析的大部分是在高层次上应用的，使得编译器成为验证链中潜在的薄弱环节。编译器中的错误特别隐蔽，因为它们很难隔离和重现，并且可能影响该编译器处理的每个程序。VeriF-OPT项目旨在通过提供一个用户友好且可重用的框架来构建编译器正确性的严格数学证明，从而使验证编译器变得可行，从而消除可能破坏高级程序验证的错误来源。VeriF-OPT项目将使用正式的方法工具，包括Isabelle证明助手和编程语言规范的K框架，开发一个通用的、可重用的框架，用于指定和验证任何语言的编译器，降低编译器验证的高门槛。该框架将被设计为特别适合并行程序的优化，因为并行程序通常比顺序程序更复杂，更难以理解。框架的核心组件是用于程序转换规范的领域特定语言，该语言的可执行语义，允许编译器设计人员在提交验证之前测试和改进他们的设计，以及作为正确性证明基础的语言的正式语义。VeriF-OPT中的每个验证都会产生代码片段、引理和其他中间结果，由于框架的模块化设计，这些结果可以在未来的项目中重用。通过帮助编译器设计人员、测试人员和验证人员一起工作来创建具有强大的正确性保证的编译器，该项目将提高软件可靠性的标准，并帮助防止由于未检测到和意外的错误而导致的昂贵和危险的失败。

The modern world runs on software, and software runs on compilers, programs that bridge the gap between human-readable high-level programming languages and the low-level machine code that computers execute. Every year, millions of dollars and countless hours of effort go into ensuring that software is correct and reliable. However, the bulk of this analysis is applied at the high level, leaving the compiler as a potential weak link in the verification chain. Errors in a compiler are particularly insidious because they are difficult to isolate and reproduce, and potentially affect every program processed by that compiler. The VeriF-OPT project aims to make it feasible to verify compilers by providing a user-friendly and reusable framework for constructing rigorous mathematical proofs of compiler correctness, thus removing a source of error that potentially undermines the verification of high-level programs.The VeriF-OPT project will use formal methods tools, including the Isabelle proof assistant and the K Framework for programming language specification, to develop a general, reusable framework for specifying and verifying compilers for any language, lowering the high barrier to entry for compiler verification. The framework will be designed to work particularly well for optimizations for parallel programs, which are often more complex and poorly understood than their sequential counterparts. The core components of the framework are a domain-specific language for the specification of program transformations, an executable semantics for this language that allows compiler designers to test and refine their designs before committing to verification, and a formal semantics for the language that serves as the basis for proofs of correctness. Every verification in VeriF-OPT will produce code fragments, lemmas, and other intermediate results that, thanks to the modular design of the framework, can be reused in future projects. By helping compiler designers, testers, and verifiers work together to create compilers with strong guarantees of correctness, the project will raise the standard for software reliability and help prevent costly and dangerous failures due to undetected and unexpected bugs.