Skip to main content

Exploiting Synchrony and Symmetry in Relational Verification

Author(s): Pick, Lauren; Fedyukovich, Grigory; Gupta, Aarti

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.
Publication Date: 2018
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
DOI: 10.1007/978-3-319-96145-3_9
ISSN: 0302-9743
EISSN: 1611-3349
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.