Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Hyperproperty Verification as CHC Satisfiability

Shachar Itzhaky, Sharon Shoham, Yakir Vizel

TL;DR

Hyperproperty verification is extended beyond single-trace properties by reducing the joint problem of trace alignment, witness selection, and relational invariants to CHC satisfiability. The paper introduces a general FO-to-CHC transformation and the notion of doomed states to enable Horn-based encoding, providing a sound and complete reduction for $k$-safety, and extends it to $ orall^* orall^*$-OHyperLTL through game semantics, including finite- and infinite-branching cases. The HyHorn tool demonstrates substantial performance gains over prior approaches by leveraging off-the-shelf CHC solvers, achieving automatic verification for many benchmarks, and enabling predicate abstraction when needed. This CHC-centric framework offers a scalable, solver-friendly pathway to relational hyperproperty verification with practical implications for security, equivalence, and robustness analyses. The work also points to future directions in automating predicate inference and extending the method to broader verification fragments.

Abstract

Hyperproperties govern the behavior of a system or systems across multiple executions, and are being recognized as an important extension of regular temporal properties. So far, such properties have resisted comprehensive treatment by modern software model-checking approaches such as IC3/PDR, due to the need to find not only an inductive invariant but also a \emph{total} alignment of different executions that facilitates simpler inductive invariants. We show how this treatment is achieved via a reduction from the verification problem of $\forall^k\exists^l$ properties to Constrained Horn Clauses. The approach is based on combining the inference of an alignment and inductive invariant in a single CHC encoding; and, for existential quantification over traces, incorporating also inference of a witness function for the existential choices, based on a game semantics with a sound-and-complete encoding to CHCs as well.

Hyperproperty Verification as CHC Satisfiability

TL;DR

Hyperproperty verification is extended beyond single-trace properties by reducing the joint problem of trace alignment, witness selection, and relational invariants to CHC satisfiability. The paper introduces a general FO-to-CHC transformation and the notion of doomed states to enable Horn-based encoding, providing a sound and complete reduction for -safety, and extends it to -OHyperLTL through game semantics, including finite- and infinite-branching cases. The HyHorn tool demonstrates substantial performance gains over prior approaches by leveraging off-the-shelf CHC solvers, achieving automatic verification for many benchmarks, and enabling predicate abstraction when needed. This CHC-centric framework offers a scalable, solver-friendly pathway to relational hyperproperty verification with practical implications for security, equivalence, and robustness analyses. The work also points to future directions in automating predicate inference and extending the method to broader verification fragments.

Abstract

Hyperproperties govern the behavior of a system or systems across multiple executions, and are being recognized as an important extension of regular temporal properties. So far, such properties have resisted comprehensive treatment by modern software model-checking approaches such as IC3/PDR, due to the need to find not only an inductive invariant but also a \emph{total} alignment of different executions that facilitates simpler inductive invariants. We show how this treatment is achieved via a reduction from the verification problem of properties to Constrained Horn Clauses. The approach is based on combining the inference of an alignment and inductive invariant in a single CHC encoding; and, for existential quantification over traces, incorporating also inference of a witness function for the existential choices, based on a game semantics with a sound-and-complete encoding to CHCs as well.
Paper Structure (37 sections, 8 theorems, 16 equations, 7 figures, 1 table)

This paper contains 37 sections, 8 theorems, 16 equations, 7 figures, 1 table.

Table of Contents

  1. Introduction
  2. Overview
  3. Motivating Example
  4. Challenges in Encoding Hyperproperty Verification as CHC-SAT
  5. Our Approach: Transformation to CHC
  6. Beyond $k$-Safety
  7. Background
  8. First Order Logic
  9. Transition Systems
  10. Hyperproperties and Their Specification
  11. Syntax
  12. Semantics
  13. Constrained Horn Clauses (CHCs)
  14. General Transformation to CHCs
  15. Encoding $k$-Safety Verification as CHCs
  16. ...and 22 more sections

Key Result

theorem 1

The set of formulas in transformation:formulas:arbiter is equi-satisfiable to the system of CHCs in transformation:formulas:doomed. Furthermore, there is an efficient translation of models of the former to models of the latter, and vice versa.

Figures (7)

  • Figure 1: (a) A program that computes the sum of squares of integer interval $[a,b)$ with a 2-safety specification for it, and (b) its first-order encoding.
  • Figure 2: CHC encoding of \ref{['intro:running-example']}.
  • Figure 3: Formula scheme before (a) and after (b) the transformation.
  • Figure 6: $k$-safety verification scheme before (a) and after (b) the transformation.
  • Figure 7: Example for a $\forall\exists$ hyperproperty.
  • ...and 2 more figures

Theorems & Definitions (21)

  • Remark 1
  • Remark 2
  • theorem 1
  • proof
  • definition 1: Arbiter
  • definition 2: Composed Transition System
  • definition 3: Valid Schedules
  • definition 4: Valid Arbiters
  • theorem 2
  • proof : Proof sketch
  • ...and 11 more