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.