Verification of the optimizing phase of a 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.