Lauren Pick will present her Pre-FPO "Scaling Automatic Verification with Domain-targeted Invariants" on Tuesday, April 20 from 1:30 to 3:30pm via Zoom. Zoom Link: https://princeton.zoom.us/j/99333126007 https://princeton.zoom.us/j/99333126007 Committee Members: Aarti Gupta (advisor, examiner) Zak Kincaid (examiner) Lennart Beringer (examiner) Andrew Appel (reader) Grigory Fedyukovich (reader, Florida State University) All are welcome to attend. Title: Scaling Automatic Verification with Domain-targeted Invariants Abstract: Automated software verification techniques, while widely successful, often suffer from scalability issues due to state-space explosion. In my thesis work, I have applied the idea of using domain insights to exploit and infer invariants, often with particular shapes, to help scale verification. In this talk, I will discuss how this approach can be used to tackle the state-space explosion problem in several domains: the verification of k-hyperproperties and safety properties for general single-threaded interprocedural programs, with special consideration for the problem of verifying information-flow security--a specific kind of 2-hyperproperty, and the verification of distributed systems. For each domain, I will highlight the specific aspects of the domain that make the invariants either easy to exploit or easy to infer and describe the exploitation or inference techniques used. I will describe how to use synchrony to infer relational invariants and how to use the symmetry within these invariants to identify and eliminate redundant verification subtasks for verifying k-hyperproperties of single-threaded programs. For safety verification of interprocedural programs, I will describe parameterizable bounded environments and how to use them to infer invariants, where the parameter helps manage the tradeoff between scalability and invariant relevance, as well as describe new forms of invariants that help handle mutual recursion. For verifying information flow security, I will show how to leverage the common structural features of information-flow properties to formulate grammar templates for inferring invariants, including those that handle quantification over array indices. Finally, I will show that for distributed systems, using a representation called a value summary to capture reachability invariants facilitates the merging of system states and their components, enabling efficient systematic exploration.