Lauren Pick General Exam Presentation - Thursday, May 10, 2018 at 3:30 pm - CS401 Title: Exploiting Synchrony and Symmetry in Relational Verification Abstract: Relational safety specifications describe multiple runs of the same program or relate the behaviors of multiple programs. Approaches to automatic relational verification often compose the programs and analyze the composition for safety, but a naively composed program can lead to difficult verification problems. In my talk, I will demonstrate two ways of exploiting relational specifications to simplify verification subtasks generated during relational verification. First, I will describe an algorithm for maximizing opportunities for synchronizing code fragments containing loops, allowing a verification procedure to avoid computing difficult loop invariants. Second, I will show how to compute symmetries in the specifications, allowing a verification procedure to avoid redundant subtasks. These enhancements have been implemented in a prototype for verifying k-safety properties on Java programs, and evaluation confirms that taking advantage of relational specifications as described leads to a consistent performance speedup on a range of benchmarks. Barbara A. Mooring Interim Graduate Coordinator Computer Science Department Princeton University