Exploiting synchrony and symmetry in relational verification

Lauren Pick, Grigory Fedyukovich, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Scopus citations

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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
EditorsGeorg Weissenbacher, Hana Chockler
PublisherSpringer Verlag
Pages164-182
Number of pages19
ISBN (Print)9783319961446
DOIs
StatePublished - 2018
Event30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom
Duration: Jul 14 2018Jul 17 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10981 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other30th International Conference on Computer Aided Verification, CAV 2018 Held as Part of the Federated Logic Conference, FloC 2018
CountryUnited Kingdom
CityOxford
Period7/14/187/17/18

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Exploiting synchrony and symmetry in relational verification'. Together they form a unique fingerprint.

Cite this