[talks] REMINDER Lauren Pick General Exam Presentation - TODAY, Thursday, May 10, 2018 at 3:30 pm - CS401

[Barbara A. Mooring]

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 describ
 ed leads to a consistent performance speedup on a range of benchmarks.


Barbara A. Mooring
Interim Graduate Coordinator
Computer Science Department
Princeton University
_______________________________________________
talks mailing list
talks at lists.cs.princeton.edu
To edit subscription settings or remove yourself, use this link:
https://lists.cs.princeton.edu/mailman/listinfo/talks