CSR---EHS: A Modern Verifying Compiler

程序是对如何操纵数据以达到某种目的的详细描述。不幸的是，程序通常不能达到程序员的预期。幸运的是，通常可以通过内联断言和函数前置条件和后置条件在逻辑上指定要做什么。函数前置条件是描述预期输入的断言，而后置条件描述返回数据和给定数据之间的关系。接下来的挑战是证明一个程序符合它的规范。众所周知，证明一个程序的每个功能都符合它的规范是无法确定的。然而，在实践中，可以分析许多程序属性。这项工作的目标是扩大可以用验证编译器大部分自动验证的程序的范围。现代验证编译器必须做好两项工作。首先，它必须通过生成归纳不变量来加强给定的注释。归纳不变量具有它最初具有的性质，并且程序的每条指令都维护它。其次，它必须证明给定的注释相对于生成的注释是归纳的，从而证明其正确性。该工作通过将基于约束的不变量生成和排序函数合成扩展到整个程序来解决第一个任务。自动不变量生成和排序函数综合减少了对超出程序规范的注释的需要。它通过寻找与验证相关的一阶理论的可表达和可判定的片段来解决第二个任务。最后，在程序验证和决策过程本科课程中使用的验证编译器中实现了理论结果。预计这将对计算机科学学科产生影响，预计将增加对专门的静态分析技术和决策程序的需求，以提高效率和准确性。这在嵌入式系统领域尤其如此，在没有分析工具辅助的情况下实现正确和可靠的系统尤其困难。

A program is a detailed description of how to manipulate data to achieve some end. Unfortunately, programs often do not achieve what their programmers intended. Fortunately, it is usually possible to specify logically what is intended through in-line assertions and function preconditions and postconditions. A function precondition is an assertion that describes the expected input, while a postcondition describes the relation between the returned data and the given data. The challenge is then to prove that a program meets its specification.It is well known that proving that each of a program's functions adheres to its specification is undecidable. In practice, though, many program properties can be analyzed. The goal of this work is to extend the range of programs that can be verified mostly automatically with a verifying compiler. A modern verifying compiler must do two tasks well. First, it must strengthen the given annotations by generating inductive invariants. An inductive invariant has the properties that it holds initially, and that each instruction of the program maintains it. Second, it must prove that the given annotations are inductive relative to the generated ones, thus proving correctness.This work addresses the first task by scaling constraint-based invariant generation and ranking function synthesis to whole programs. Automatic invariant generation and ranking function synthesis reduces the need for annotations beyond the program specification. It addresses the second task by finding expressive and decidable fragments of first-order theories relevant for verification. Finally, the theoretical results are implemented in a verifying compiler that is used in an undergraduate course on program verification and decision procedures. This is expected to have impact for the discipline of Computer Science, where increased demand is predicted for specialized static analysis techniques and decision procedures that will improve efficiency and accuracy. This is especially true in the area of embedded systems, where achieving correct and reliable systems without the assistance of analysis tools is particularly difficult.