Please note revised changes to include Zoom Link and Event Attendance Requirement: ---------------------------------------------------------------------------- -------------------------------------------- Lauren Pick will present her FPO "Scaling Automatic Modular Verification" on Tuesday, November 2, 2021 at 3PM at Friend 101 and via Zoom. Location: Friend 101 Zoom Link: https://princeton.zoom.us/j/98885075628 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 mailto:gradinfo@cs.princeton.edu if you would like a copy of the thesis. Everyone is invited to attend her talk. Please note: For in-person meetings on campus such as the FPO, it is required that all attendees complete an event attendance sheet attesting that they are fully vaccinated for COVID-19. A sample of the form is attached for your information. A copy of the form will be circulated and will need to be filled out by all in-person attendees prior to the start of the FPO. 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.