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.

翻译：超性质管辖着一个或多个系统在多次执行中的行为，并被公认为常规时态性质的重要扩展。然而，由于这类性质不仅需要寻找归纳不变式，还需建立不同执行间的全局对齐以支持更简洁的归纳不变式，因此至今未能被IC3/PDR等现代软件模型检测方法全面处理。本文展示了如何通过将∀ᵏ∃ˡ性质验证问题归约为约束Horn子句来实现这一处理。该方法的核心在于将对齐推理与归纳不变式推断统一编码为单一CHC约束系统；针对迹上的存在量词，进一步基于博弈语义引入存在性选择见证函数的推断，该语义同样得以完备且正确地编码为CHC公式。