Verification of the optimizing phase of a compiler

编译器优化阶段的验证

• 批准号: EP/D032466/1
• 负责人: Sara Kalvala
• 金额: $ 10.04万
• 依托单位: University of Warwick
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2006
• 资助国家: 英国
• 起止时间: 2006 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FD032466%2F1
• 关键词: Verification; optimizing; phase; compiler

Computer programs are sets of instructions to make a computer perform a certain task. We write these programs in programming languages that are easy for humans to understand. Computers, however, are simple and want very simple instructions to run (for example, ones that involve just moving, adding or subtracting numbers). So to get programs to run, we need to convert our human readable programs into these simple instructions. To do this we use another computer program called a compiler.It is important that this conversion process does not go wrong - otherwise the computer will not do what we expect it to do. However, compilers are very complicated programs, sometimes having to deal with millions of instructions; it is very hard to know whether the translation is going wrong. Also, most compilers are clever and attempt to improve the program as it is translated. They try to make the program more efficient and that complicates things even further / making it even harder to know whether the translation is correct or not.Luckily, computer programs can be viewed as mathematical objects (like numbers, formulas and equations) and therefore we can prove things about them. This research aims to find ways to prove that compilers do not go wrong - they always do a correct translation. In particular, the research looks at how to prove this even when the compiler is trying to improve the program.

计算机程序是使计算机执行特定任务的指令集。我们用人类易于理解的编程语言编写这些程序。然而，计算机很简单，需要非常简单的指令来运行（例如，那些只涉及移动，添加或减去数字的指令）。为了让程序运行，我们需要将人类可读的程序转换成这些简单的指令。为了做到这一点，我们使用了另一个叫做编译器的计算机程序，重要的是这个转换过程不能出错，否则计算机就不会做我们期望它做的事情。然而，编译器是非常复杂的程序，有时必须处理数百万条指令;很难知道翻译是否出错。此外，大多数编译器都很聪明，并试图在翻译程序时对其进行改进。他们试图使程序更有效率，这使事情变得更加复杂/使它更难知道翻译是否正确。幸运的是，计算机程序可以被视为数学对象（如数字，公式和方程），因此我们可以证明它们的东西。这项研究旨在找到方法来证明编译器不会出错-他们总是做正确的翻译。特别是，研究着眼于如何证明这一点，即使编译器试图改善程序。

项目成果

Program transformations using temporal logic side conditions

使用时序逻辑辅助条件进行程序转换

• DOI: 10.1145/1516507.1516509
• 发表时间: 2009
• 期刊: ACM Transactions on Programming Languages and Systems
• 影响因子: 1.3
• 作者: Kalvala S

Towards the automated correction of bugs

• 发表时间: 2009-12
• 作者: Richard Warburton;Sara Kalvala

Verifying Compiling Optimisations Using Isabelle/HOL

使用 Isabelle/HOL 验证编译优化

• 发表时间: 2009
• 作者: R Warburton

Compiler Construction

编译器构建

• DOI: 10.1007/978-3-540-71229-9_15
• 发表时间: 2007
• 作者: Falconer H