CSR---EHS: A Modern Verifying Compiler

Stanford University, Stanford CA

Investigators

Abstract

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.