Lauren Pick will present her FPO "Scaling Automatic Modular Verification" on Tuesday, November 2, 2021 at 3PM at Friend 101.

Location: Friend 101

The members of Lauren’s committee are as follows:

Examiners: Aarti Gupta (Adviser), E. Lennart Beringer and Zachary Kincaid

Readers: Andrew Appel and Grigory Fedyukovich (Florida State University)

A copy of her thesis is available upon request.  Please email gradinfo@cs.princeton.edu if you would like a copy of the thesis.

Everyone is invited to attend her talk.

Abstract follows below:

Automated software verification techniques, while widely successful, often suffer from scalability issues due to state-space explosion. In both automated and manual verification, modular approaches help scale verification by breaking verification problems into several easier-to-solve subproblems. These subproblems often involve discovering suitable invariants that can be used to help derive a proof that the entire system meets the desired specification.

In this dissertation, I describe work toward developing modular automatic techniques for software verification in which such invariants are discovered automatically. These techniques notably involve exploiting the structure and syntax of both system components and/or their specifications in order to find useful invariants for scaling verification. I have developed techniques for several related kinds of verification problems: the verification of k-safety properties, the verification of safety properties for general single-threaded interprocedural programs, and the verification of information-flow security—a specific kind of 2-safety property.

For each of these verification problems, I have implemented the developed techniques in a verification tool and compared the tool to existing state-of-the-art tools for solving the verification problem. Experimental results demonstrate that the developed techniques help scale verification over existing state-of-the-art and allow more verification problems to be solved automatically.