Reductions for Automated Hypersafety Verification
Abstract
We propose an automated verification technique for hypersafety properties, which express sets of valid interrelations between multiple finite runs of a program. The key observation is that constructing a proof for a small representative set of the runs of the product program (i.e. the product of the several copies of the program by itself), called a reduction, is sufficient to formally prove the hypersafety property about the program. We propose an algorithm based on a counterexample-guided refinement loop that simultaneously searches for a reduction and a proof of the correctness for the reduction. We demonstrate that our tool Weaver is very effective in verifying a diverse array of hypersafety properties for a diverse class of input programs.
Cite
@article{arxiv.1905.09242,
title = {Reductions for Automated Hypersafety Verification},
author = {Azadeh Farzan and Anthony Vandikas},
journal= {arXiv preprint arXiv:1905.09242},
year = {2019}
}