Reasoning About Hyperproperties with Automated Theorem Provers (extended version)

EasyChair Preprint 16030

Abstract

We present a benchmark suite and an accompanying experimental study that assesses the capabilities of modern Automated Theorem Provers (ATPs) for hyperproperty reasoning. Existing tools for reasoning about hyperproperties typically rely on specialised model checkers or a custom encoding to satisfiability modulo theories (SMT) solvers or first-order provers. Our suite constitutes the first systematic collection of Smt-Lib encodings spanning hyperproperty satisfiability, model checking, and software verification via Constrained Horn Clauses (CHCs). Using this suite, we evaluate state-of-the-art ATPs, including SMT solvers and first-order theorem provers, that support both arithmetic and quantified reasoning. Beyond measuring how different solvers perform, we summarize lessons we learned on what makes a good encoding and solver configuration for hyperproperties. The benchmark suite, translation scripts, and experimental setup are released as an open artifact, enabling reproducible evaluation and providing a foundation for future improvements in automated reasoning about hyperproperties. This paper is the extended version of a paper with the same title which will be published at LPAR 2026.

Keyphrases: Benchmarks, Hyperproperties, SMT, automated theorem provers, model checking, software verification

@booklet{EasyChair:16030,
  author    = {Tobias Nießen and Ana Oliveira da Costa and Johannes Schoisswohl and Thomas A. Henzinger and Laura Kovács},
  title     = {Reasoning About Hyperproperties with Automated Theorem Provers (extended version)},
  howpublished = {EasyChair Preprint 16030},
  year      = {EasyChair, 2026}}