PhD Proposal: Mechanizing Abstract Interpretation

Program analyzers have proven effective in verifying the absense of undesirable software behavior such as crashes, bugs and security vulnerabilities. Some settings require high assurance in the results of program analysis predictions, e.g. an analyzer for embedded software in automobiles or airplanes. To achieve high assurance in a program analyzer, formal methods are used to automatically construct or check proofs of its correctness.
Achieving high assurance for a program analyzer is a challenging task, and current methods are not suitable for mainstream use. As a result, verification is only attempted for analyzers which are both extremely critical and relataively simple. In this thesis, I describe how to bring verified program analyzers closer to a reality for mainstream use by improving the methods used to develop their implementations and proofs.
There are two fundamental challenges in the state of the art for designing mechanically verified program analyzers: (1) small changes to program analyzers require large changes in their proofs; and (2) a proof for a program analyzer takes much more effort to complete than its implementation.

I improve on (1) by demonstrating how to design program analyzers which are compositional, extensible and amenable to verification, a combination the first of its kind. Compositionality and extensibility allow for one to rapidly prototype the design space of program analyzers without requiring large changes to the proof of its correctness. Our contributions which enable these features are Galois Transformers and Abstract Definitional Interpreters. Both results identify components of program analyzers which are orthogonal, and support mechanization of each component in isolation of the others. By combining the mechanization of each isolated component, an end-to-end guarantee of correctness for the resulting program analyzer is synthesized without additional proof effort.

I improve on (2) by developing a new theoretical framework for deriving verified program analyzers directly from their specifications, and in a way that supports mechanized verification. Previous approaches to correct-by-construction program derivation for program analyzers cannot be mechanized effectively due to foundational limitations, which our framework overcomes. Our contribution which underlies this new approach is Constructive Galois Connections, which recasts the classical theory of Galois connections into an explicitly constructive mathematical setting. Using constructive Galois connections, program analyzers are calculated directly from their specifications, and the results are simultaneously correct-by-construction and immediately executable as algorithms.

Examining Committee:

Chair: Dr. David Van Horn

Dept rep: Dr. Hal Daume III

Members: Dr. Jeff Foster

Dr. Mike Hicks