To refer to this page use:
|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 result for safety, but a naively composed program can lead to difficult verification problems. We propose to exploit relational specifications for simplifying the generated verification subtasks. First, we maximize opportunities for synchronizing code fragments. Second, we compute symmetries in the specifications to reveal and avoid redundant subtasks. We have implemented these enhancements in a prototype for verifying k-safety properties on Java programs. Our evaluation confirms that our approach leads to a consistent performance speedup on a range of benchmarks.|
|Citation:||Pick, Lauren, Grigory Fedyukovich, and Aarti Gupta. "Exploiting Synchrony and Symmetry in Relational Verification." In International Conference on Computer Aided Verification (2018): pp. 164-182. doi:10.1007/978-3-319-96145-3_9|
|Pages:||164 - 182|
|Type of Material:||Conference Article|
|Journal/Proceeding Title:||International Conference on Computer Aided Verification|
|Version:||Final published version. This is an open access article.|
Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.