# Reductions for Automated Hypersafety Verification

## TL;DR

This paper introduces an automated verification method for hypersafety properties, using reductions to simplify the proof process by analyzing a representative set of program runs, demonstrated with the tool Weaver.

## Contribution

It presents a novel reduction-based approach for hypersafety verification and an algorithm that combines reduction search with proof generation in a counterexample-guided loop.

## Key findings

- Weaver effectively verifies diverse hypersafety properties.
- The reduction approach simplifies complex hypersafety proofs.
- The method is applicable to various classes of input programs.

## 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.