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

SHF：小型：VeriF-OPT，优化和程序转换的验证框架

• 批准号: 1318191
• 负责人: Elsa Gunter
• 金额: $ 46.6万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-09-01 至 2017-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1318191&HistoricalAwards=false
• 关键词: SHF; Small; VeriF; OPT; Verification

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.

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